helm/software/matita/tests/pullback.ma

   1
   2 (*
   3 axiom A : Type.
   4 axiom B : Type.
   5 axiom B1 : Type.
   6 axiom C : Type.
   7
   8 axiom f1 : A → B.
   9 axiom f2 : A → B1.
  10 axiom f3 : B → C.
  11 axiom f4 : B1 → C.
  12
  13 coercion f1.
  14 coercion f2.
  15 coercion f3.
  16 coercion f4.
  17
  18
  19
  20
  21 axiom P : Prop.
  22
  23 lemma x : P.
  24 *)
  25
  26 include "logic/equality.ma".
  27
  28 record L : Type \def {
  29   l_c : Prop;
  30   l_op : l_c \to l_c \to l_c
  31 }.
  32
  33 record R : Type \def {
  34   r_c : Prop;
  35   r_op : r_c \to r_c \to r_c
  36 }.
  37
  38 record LR_ : Type \def {
  39   lr_L : L ;
  40   lr_R_ : R ;
  41   lr_w : r_c lr_R_ = l_c lr_L
  42 }.
  43
  44 lemma lr_R : LR_ \to R.
  45 intros;constructor 1;
  46 [apply rule (l_c (lr_L l))
  47 |rewrite < (lr_w l);apply (r_op (lr_R_ l));]
  48 qed.
  49
  50 (*
  51 axiom F : Prop → Prop.
  52 axiom C : Prop → Prop.
  53
  54 axiom daemon : ∀x.F x = C x.
  55
  56 lemma xxx : ∀x.F x = C x. apply daemon; qed.
  57
  58 axiom yyyy : ∀x.C (C x) = C (C x) → F (F x) = F (F x).
  59
  60 coercion yyyy.
  61
  62 lemma x : ∀x. (λy:F (F x) = F (F x).True) (refl_eq ? (C (C x))).
  63
  64 include "nat/factorial.ma".
  65 lemma xxx : 8! = 8 * 7!. intros; reflexivity; qed.
  66
  67 lemma x : (λy:8!=8!.True) (refl_eq ? (8 * 7!)).
  68 apply (refl_eq ??);
  69 *)
  70
  71 (*
  72 lemma xxx : \forall x. r_c (lr_R x) = l_c (lr_L x).
  73 intros; reflexivity;
  74 qed.
  75 *)
  76
  77
  78
  79 definition Prop_OR_LR_1 : LR_ → Prop.
  80 apply (λx.r_c (lr_R x)).
  81 qed.
  82
  83 (*
  84 coercion Prop_OR_LR_1.
  85 coercion lr_R.
  86 *)
  87
  88 unification hint (\forall x. r_c (lr_R x) = l_c (lr_L x)).
  89
  90 lemma foo : \forall x,y.l_op ? x (r_op ? x y) = x.
  91
  92 r_c ?1 =?= l_c ?2
  93
  94
  95 r_c (lr_R ?3) === l_c (lr_L ?3)
  96 r_c (lr_R ?) === l_c (lr_L ?)   |---->
  97    \forall x. r_c (lr_R x) === l_c (lr_L x)
  98
  99
 100 inductive T : Type \def t : T.
 101 inductive L : Type \def l : L.
 102 inductive R : Type \def r : R.
 103 inductive R1 : Type \def r1 : R1.
 104 inductive P1 : Type \def p1 : P1.
 105 inductive P2 : Type \def p2 : P2.
 106
 107 definition L_to_T : L \to T \def \lambda x.t.
 108 definition R_to_T : R \to T \def \lambda x.t.
 109 definition P1_to_L : P1 \to L \def \lambda x.l.
 110 definition P1_to_R1 : P1 \to R1 \def \lambda x.r1.
 111 definition R1_to_P2 : R1 \to P2 \def \lambda x.p2.
 112 definition R1_to_R : R1 \to R \def \lambda x.r.
 113 definition P2_to_L : P2 \to L \def \lambda x.l.
 114 definition P2_to_R : P2 \to R \def \lambda x.r.
 115 definition P1_to_P1 : P1 \to P1 \def \lambda x.p1.
 116
 117 coercion cic:/matita/tests/pullback/L_to_T.con.
 118 coercion cic:/matita/tests/pullback/R_to_T.con.
 119 coercion cic:/matita/tests/pullback/P1_to_L.con.
 120 coercion cic:/matita/tests/pullback/P1_to_R1.con.
 121 coercion cic:/matita/tests/pullback/R1_to_R.con.
 122 coercion cic:/matita/tests/pullback/R1_to_P2.con.
 123 coercion cic:/matita/tests/pullback/P2_to_L.con.
 124 coercion cic:/matita/tests/pullback/P2_to_R.con.
 125 coercion cic:/matita/tests/pullback/P1_to_P1.con.