From: Enrico Tassi Date: Wed, 8 Sep 2010 13:30:32 +0000 (+0000) Subject: ... X-Git-Tag: make_still_working~2840 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=070b44c9c2344967ca8c4531909614a0d4da2fbe;p=helm.git ... --- diff --git a/helm/software/matita/nlibrary/re/re-setoids.ma b/helm/software/matita/nlibrary/re/re-setoids.ma index 28332fbff..06791066a 100644 --- a/helm/software/matita/nlibrary/re/re-setoids.ma +++ b/helm/software/matita/nlibrary/re/re-setoids.ma @@ -25,9 +25,8 @@ ninductive list (A:Type[0]) : Type[0] ≝ nlet rec eq_list (A : setoid) (l1, l2 : list A) on l1 : CProp[0] ≝ match l1 with -[ nil ⇒ match l2 return λ_.CProp[0] with [ nil ⇒ ? | _ ⇒ ? ] -| cons x xs ⇒ match l2 with [ nil ⇒ ? | cons y ys ⇒ x = y ∧ eq_list ? xs ys]]. -##[ napply True|napply False|napply False]nqed. +[ nil ⇒ match l2 return λ_.CProp[0] with [ nil ⇒ True | _ ⇒ False ] +| cons x xs ⇒ match l2 with [ nil ⇒ False | cons y ys ⇒ x = y ∧ eq_list ? xs ys]]. ndefinition LIST : setoid → setoid. #S; @(list S); @(eq_list S); ncases admit; nqed. @@ -322,14 +321,41 @@ ndefinition ex_morph : ∀S:setoid. (S ⇒_1 CPROP) ⇒_1 CPROP. *; #x; #H; @ x; nlapply (E x x ?); //; *; /2/; nqed. -nlemma Sig: ∀S,T:setoid.∀P: S → (T → CProp[0]). +nlemma Sig: ∀S,T:setoid.∀P: S → (T → CPROP). ∀y,z:T.y = z → (∀x.y=z → P x y = P x z) → (Ex S (λx.P x y)) =_1 (Ex S (λx.P x z)). #S T P y z Q E; @; *; #x Px; @x; nlapply (E x Q); *; /2/; nqed. +(* desiderata : Σ(λx.H‡#) + ottenute : Σ H (λx,H.H‡#) -- quindi monoriscrittura. H toplevel permette inferenza di y e z in Sig +*) nlemma test : ∀S:setoid. ∀ee: S ⇒_1 S ⇒_1 CPROP. ∀x,y:setoid1_of_setoid S.x =_1 y → (Ex S (λw.ee x w ∧ True)) =_1 (Ex S (λw.ee y w ∧ True)). #S m x y E; + +napply (trans1 ????? (Sig ????? E (λw,H. + (prop11 ?(unary_morphism1_setoid1 ??)??? + (prop11 ?(unary_morphism1_setoid1 ??)??? + H + ?? (refl ???)) + ?? (refl1 ???))))). +napply refl1. +nqed. + +nlemma test2 : ∀S:setoid. ∀ee: S ⇒_1 S ⇒_1 CPROP. + ∀x,y:setoid1_of_setoid S.x =_1 y → + (True ∧ (Ex S (λw.ee x w ∧ True))) =_1 (True ∧ (Ex S (λw.ee y w ∧ True))). +#S m x y E; +napply (trans1 ????? +(#‡ + (Sig ????? E (λw,H. + (prop11 ?(unary_morphism1_setoid1 ??)??? + (prop11 ?(unary_morphism1_setoid1 ??)??? + H + ?? (refl ???)) + ?? (refl1 ???)))))). +napply refl1. + alias symbol "trans" (instance 1) = "trans1". alias symbol "refl" (instance 5) = "refl". alias symbol "prop2" (instance 3) = "prop21". @@ -349,7 +375,37 @@ alias symbol "prop2" (instance 3) = "prop21". la E astratta nella prova è solo per fargli inferire x e y, se Sig lo si riformula in modo più naturale (senza y=z) allora bisogna passare x e y esplicitamente. *) -napply (.= (Sig ? S (λw,x.(m x w) ∧ True) ?? E (λw,E.(E‡#)‡#))); +alias symbol "trans" (instance 1) = "trans1". +alias symbol "prop2" (instance 3) = "prop21". +alias symbol "trans" (instance 1) = "trans1". +alias symbol "prop2" (instance 3) = "prop21". + +alias symbol "trans" (instance 1) = "trans1". +alias symbol "prop2" (instance 3) = "prop21". +(*napply (.= (Sig ? S (λw,x. m x w ∧ True) ?? E (λw,H.(H‡#)‡#))); *) + +(* OK *) +napply (.= (Sig ? ? (?) ?? E (λw,H. + (prop11 ?(unary_morphism1_setoid1 ??)??? + (prop11 ?(unary_morphism1_setoid1 ??)??? + H + ?? (refl ???)) + ?? (refl1 ???))))). +napply refl1. + + (prop11 (setoid1_of_setoid ?) (ext_powerclass_setoid ?) ? ? ???? + (prop11 (setoid1_of_setoid ?) (ext_powerclass_setoid ?) ? ? ???? + H + (refl ??)) + (refl ? True))))). + +prop11 ???????? (prop11 ???????? H (refl ??)) (refl ??)))); + +napply (.= (Sig ? S (λw,x. m x w ∧ True) ?? E (λw,H.(H‡#)‡#))); + + +napply (.= (Sig ? S (λw,x.?) ?? E (λw,H.(H‡#)‡#))); +(Ex S (λx.?P x y)) ==?== //; nqed. STOP napply (λw:S.(.= ((E‡#)‡#)) #); ##[##2: napply w| napply m. #H; napply H;