matita/matita/contribs/lambdadelta/legacy_1/coq/fwd.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/coq/defs.ma".
  18
  19 theorem False_rect:
  20  \forall (P: Type[0]).(False \to P)
  21 \def
  22  \lambda (P: Type[0]).(\lambda (f: False).(match f in False with [])).
  23
  24 theorem False_ind:
  25  \forall (P: Prop).(False \to P)
  26 \def
  27  \lambda (P: Prop).(False_rect P).
  28
  29 theorem land_rect:
  30  \forall (A: Prop).(\forall (B: Prop).(\forall (P: Type[0]).(((A \to (B \to
  31 P))) \to ((land A B) \to P))))
  32 \def
  33  \lambda (A: Prop).(\lambda (B: Prop).(\lambda (P: Type[0]).(\lambda (f: ((A
  34 \to (B \to P)))).(\lambda (a: (land A B)).(match a with [(conj x x0)
  35 \Rightarrow (f x x0)]))))).
  36
  37 theorem land_ind:
  38  \forall (A: Prop).(\forall (B: Prop).(\forall (P: Prop).(((A \to (B \to P)))
  39 \to ((land A B) \to P))))
  40 \def
  41  \lambda (A: Prop).(\lambda (B: Prop).(\lambda (P: Prop).(land_rect A B P))).
  42
  43 theorem or_ind:
  44  \forall (A: Prop).(\forall (B: Prop).(\forall (P: Prop).(((A \to P)) \to
  45 (((B \to P)) \to ((or A B) \to P)))))
  46 \def
  47  \lambda (A: Prop).(\lambda (B: Prop).(\lambda (P: Prop).(\lambda (f: ((A \to
  48 P))).(\lambda (f0: ((B \to P))).(\lambda (o: (or A B)).(match o with
  49 [(or_introl x) \Rightarrow (f x) | (or_intror x) \Rightarrow (f0 x)])))))).
  50
  51 theorem ex_ind:
  52  \forall (A: Type[0]).(\forall (P: ((A \to Prop))).(\forall (P0:
  53 Prop).(((\forall (x: A).((P x) \to P0))) \to ((ex A P) \to P0))))
  54 \def
  55  \lambda (A: Type[0]).(\lambda (P: ((A \to Prop))).(\lambda (P0:
  56 Prop).(\lambda (f: ((\forall (x: A).((P x) \to P0)))).(\lambda (e: (ex A
  57 P)).(match e with [(ex_intro x x0) \Rightarrow (f x x0)]))))).
  58
  59 theorem ex2_ind:
  60  \forall (A: Type[0]).(\forall (P: ((A \to Prop))).(\forall (Q: ((A \to
  61 Prop))).(\forall (P0: Prop).(((\forall (x: A).((P x) \to ((Q x) \to P0))))
  62 \to ((ex2 A P Q) \to P0)))))
  63 \def
  64  \lambda (A: Type[0]).(\lambda (P: ((A \to Prop))).(\lambda (Q: ((A \to
  65 Prop))).(\lambda (P0: Prop).(\lambda (f: ((\forall (x: A).((P x) \to ((Q x)
  66 \to P0))))).(\lambda (e: (ex2 A P Q)).(match e with [(ex_intro2 x x0 x1)
  67 \Rightarrow (f x x0 x1)])))))).
  68
  69 theorem eq_rect:
  70  \forall (A: Type[0]).(\forall (x: A).(\forall (P: ((A \to Type[0]))).((P x)
  71 \to (\forall (y: A).((eq A x y) \to (P y))))))
  72 \def
  73  \lambda (A: Type[0]).(\lambda (x: A).(\lambda (P: ((A \to
  74 Type[0]))).(\lambda (f: (P x)).(\lambda (y: A).(\lambda (e: (eq A x
  75 y)).(match e with [refl_equal \Rightarrow f])))))).
  76
  77 theorem eq_ind:
  78  \forall (A: Type[0]).(\forall (x: A).(\forall (P: ((A \to Prop))).((P x) \to
  79 (\forall (y: A).((eq A x y) \to (P y))))))
  80 \def
  81  \lambda (A: Type[0]).(\lambda (x: A).(\lambda (P: ((A \to Prop))).(eq_rect A
  82 x P))).
  83
  84 let rec le_ind (n: nat) (P: (nat \to Prop)) (f: P n) (f0: (\forall (m:
  85 nat).((le n m) \to ((P m) \to (P (S m)))))) (n0: nat) (l: le n n0) on l: P n0
  86 \def match l with [le_n \Rightarrow f | (le_S m l0) \Rightarrow (f0 m l0
  87 ((le_ind n P f f0) m l0))].
  88
  89 let rec Acc_ind (A: Type[0]) (R: (A \to (A \to Prop))) (P: (A \to Prop)) (f:
  90 (\forall (x: A).(((\forall (y: A).((R y x) \to (Acc A R y)))) \to (((\forall
  91 (y: A).((R y x) \to (P y)))) \to (P x))))) (a: A) (a0: Acc A R a) on a0: P a
  92 \def match a0 with [(Acc_intro x a1) \Rightarrow (f x a1 (\lambda (y:
  93 A).(\lambda (r0: (R y x)).((Acc_ind A R P f) y (a1 y r0)))))].
  94