From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Mon, 15 Dec 2008 19:20:08 +0000 (+0000)
Subject: Some changes to the pullback test, for debugging
X-Git-Tag: make_still_working~4391
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dc71aab016c7d379e82eea08c4425ab763c593ac;p=helm.git

Some changes to the pullback test, for debugging
---

diff --git a/helm/software/matita/tests/pullback.ma b/helm/software/matita/tests/pullback.ma
index 1196255d9..d224e6b0e 100644
--- a/helm/software/matita/tests/pullback.ma
+++ b/helm/software/matita/tests/pullback.ma
@@ -12,6 +12,48 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "logic/equality.ma".
+
+record L : Type \def {
+  l_c :> Prop;
+  l_op : l_c \to l_c \to l_c
+}.
+
+record R : Type \def {
+  r_c :> Prop;
+  r_op : r_c \to r_c \to r_c
+}.
+
+record LR_ : Type \def {
+  lr_L : L ;
+  lr_R_ : R ;
+  lr_w : r_c lr_R_ = l_c lr_L
+}.
+
+lemma lr_R : LR_ \to R.
+intros;constructor 1;
+[apply rule (lr_L l)
+|rewrite < (lr_w l);apply (r_op (lr_R_ l));]
+qed.
+
+lemma xxx : \forall x. r_c (lr_R x) = l_c (lr_L x).
+intros; reflexivity;
+qed.
+
+coercion lr_L.
+
+
+
+coercion lr_R.
+
+lemma foo : \forall x,y.l_op ? x (r_op ? x y) = x.
+
+r_c ?1 =?= l_c ?2
+
+
+r_c (lr_R ?3) === l_c (lr_L ?3)
+r_c (lr_R ?) === l_c (lr_L ?)   |---->   
+   \forall x. r_c (lr_R x) === l_c (lr_L x)
 
 
 inductive T : Type \def t : T.