From dc71aab016c7d379e82eea08c4425ab763c593ac Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Mon, 15 Dec 2008 19:20:08 +0000 Subject: [PATCH] Some changes to the pullback test, for debugging --- helm/software/matita/tests/pullback.ma | 42 ++++++++++++++++++++++++++ 1 file changed, 42 insertions(+) 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. -- 2.39.2