matita/matita/contribs/lambdadelta/legacy_1/coq/defs.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "legacy_1/preamble.ma".
  18
  19 inductive eq (A: Type[0]) (x: A): A \to Prop \def
  20 | refl_equal: eq A x x.
  21
  22 inductive True: Prop \def
  23 | I: True.
  24
  25 inductive land (A: Prop) (B: Prop): Prop \def
  26 | conj: A \to (B \to (land A B)).
  27
  28 inductive or (A: Prop) (B: Prop): Prop \def
  29 | or_introl: A \to (or A B)
  30 | or_intror: B \to (or A B).
  31
  32 inductive ex (A: Type[0]) (P: A \to Prop): Prop \def
  33 | ex_intro: \forall (x: A).((P x) \to (ex A P)).
  34
  35 inductive ex2 (A: Type[0]) (P: A \to Prop) (Q: A \to Prop): Prop \def
  36 | ex_intro2: \forall (x: A).((P x) \to ((Q x) \to (ex2 A P Q))).
  37
  38 definition not:
  39  Prop \to Prop
  40 \def
  41  \lambda (A: Prop).(A \to False).
  42
  43 inductive bool: Type[0] \def
  44 | true: bool
  45 | false: bool.
  46
  47 inductive nat: Type[0] \def
  48 | O: nat
  49 | S: nat \to nat.
  50
  51 inductive le (n: nat): nat \to Prop \def
  52 | le_n: le n n
  53 | le_S: \forall (m: nat).((le n m) \to (le n (S m))).
  54
  55 definition lt:
  56  nat \to (nat \to Prop)
  57 \def
  58  \lambda (n: nat).(\lambda (m: nat).(le (S n) m)).
  59
  60 definition IsSucc:
  61  nat \to Prop
  62 \def
  63  \lambda (n: nat).(match n with [O \Rightarrow False | (S _) \Rightarrow
  64 True]).
  65
  66 definition pred:
  67  nat \to nat
  68 \def
  69  \lambda (n: nat).(match n with [O \Rightarrow O | (S u) \Rightarrow u]).
  70
  71 rec definition plus (n: nat) on n: nat \to nat \def \lambda (m: nat).(match n
  72 with [O \Rightarrow m | (S p) \Rightarrow (S (plus p m))]).
  73
  74 rec definition minus (n: nat) on n: nat \to nat \def \lambda (m: nat).(match
  75 n with [O \Rightarrow O | (S k) \Rightarrow (match m with [O \Rightarrow (S
  76 k) | (S l) \Rightarrow (minus k l)])]).
  77
  78 inductive Acc (A: Type[0]) (R: A \to (A \to Prop)): A \to Prop \def
  79 | Acc_intro: \forall (x: A).(((\forall (y: A).((R y x) \to (Acc A R y)))) \to
  80 (Acc A R x)).
  81
  82 definition well_founded:
  83  \forall (A: Type[0]).(((A \to (A \to Prop))) \to Prop)
  84 \def
  85  \lambda (A: Type[0]).(\lambda (R: ((A \to (A \to Prop)))).(\forall (a:
  86 A).(Acc A R a))).
  87
  88 definition ltof:
  89  \forall (A: Type[0]).(((A \to nat)) \to (A \to (A \to Prop)))
  90 \def
  91  \lambda (A: Type[0]).(\lambda (f: ((A \to nat))).(\lambda (a: A).(\lambda
  92 (b: A).(lt (f a) (f b))))).
  93