helm/software/matita/tests/pullback.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 include "logic/equality.ma".
  16
  17 record L : Type \def {
  18   l_c :> Prop;
  19   l_op : l_c \to l_c \to l_c
  20 }.
  21
  22 record R : Type \def {
  23   r_c :> Prop;
  24   r_op : r_c \to r_c \to r_c
  25 }.
  26
  27 record LR_ : Type \def {
  28   lr_L : L ;
  29   lr_R_ : R ;
  30   lr_w : r_c lr_R_ = l_c lr_L
  31 }.
  32
  33 lemma lr_R : LR_ \to R.
  34 intros;constructor 1;
  35 [apply rule (lr_L l)
  36 |rewrite < (lr_w l);apply (r_op (lr_R_ l));]
  37 qed.
  38
  39 lemma xxx : \forall x. r_c (lr_R x) = l_c (lr_L x).
  40 intros; reflexivity;
  41 qed.
  42
  43 coercion lr_L.
  44
  45
  46
  47 coercion lr_R.
  48
  49 lemma foo : \forall x,y.l_op ? x (r_op ? x y) = x.
  50
  51 r_c ?1 =?= l_c ?2
  52
  53
  54 r_c (lr_R ?3) === l_c (lr_L ?3)
  55 r_c (lr_R ?) === l_c (lr_L ?)   |---->
  56    \forall x. r_c (lr_R x) === l_c (lr_L x)
  57
  58
  59 inductive T : Type \def t : T.
  60 inductive L : Type \def l : L.
  61 inductive R : Type \def r : R.
  62 inductive R1 : Type \def r1 : R1.
  63 inductive P1 : Type \def p1 : P1.
  64 inductive P2 : Type \def p2 : P2.
  65
  66 definition L_to_T : L \to T \def \lambda x.t.
  67 definition R_to_T : R \to T \def \lambda x.t.
  68 definition P1_to_L : P1 \to L \def \lambda x.l.
  69 definition P1_to_R1 : P1 \to R1 \def \lambda x.r1.
  70 definition R1_to_P2 : R1 \to P2 \def \lambda x.p2.
  71 definition R1_to_R : R1 \to R \def \lambda x.r.
  72 definition P2_to_L : P2 \to L \def \lambda x.l.
  73 definition P2_to_R : P2 \to R \def \lambda x.r.
  74 definition P1_to_P1 : P1 \to P1 \def \lambda x.p1.
  75
  76 coercion cic:/matita/tests/pullback/L_to_T.con.
  77 coercion cic:/matita/tests/pullback/R_to_T.con.
  78 coercion cic:/matita/tests/pullback/P1_to_L.con.
  79 coercion cic:/matita/tests/pullback/P1_to_R1.con.
  80 coercion cic:/matita/tests/pullback/R1_to_R.con.
  81 coercion cic:/matita/tests/pullback/R1_to_P2.con.
  82 coercion cic:/matita/tests/pullback/P2_to_L.con.
  83 coercion cic:/matita/tests/pullback/P2_to_R.con.
  84 coercion cic:/matita/tests/pullback/P1_to_P1.con.