X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdemo%2Ftoolbox.ma;h=adc6b1d83650d13ae19febc219ec1e805e9cc960;hb=070b44c9c2344967ca8c4531909614a0d4da2fbe;hp=7ee9e5da7f3d4fa4fb81e1078fa759f85d974cb8;hpb=00c99933872f0eb457e62354cc1a317e4359188e;p=helm.git diff --git a/helm/software/matita/library/demo/toolbox.ma b/helm/software/matita/library/demo/toolbox.ma index 7ee9e5da7..adc6b1d83 100644 --- a/helm/software/matita/library/demo/toolbox.ma +++ b/helm/software/matita/library/demo/toolbox.ma @@ -14,6 +14,8 @@ include "logic/cprop_connectives.ma". +axiom daemon: False. + record iff (A,B: CProp) : CProp ≝ { if: A → B; fi: B → A @@ -29,6 +31,10 @@ for @{ 'iff $a $b }. interpretation "logical iff" 'iff x y = (iff x y). +definition reflexive1 ≝ λA:Type.λR:A→A→CProp.∀x:A.R x x. +definition symmetric1 ≝ λC:Type.λlt:C→C→CProp. ∀x,y:C.lt x y → lt y x. +definition transitive1 ≝ λA:Type.λR:A→A→CProp.∀x,y,z:A.R x y → R y z → R x z. + record setoid : Type ≝ { carr:> Type; eq: carr → carr → CProp; @@ -42,7 +48,6 @@ definition proofs: CProp → setoid. constructor 1; [ apply A | intros; - alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)". apply True | intro; constructor 1 @@ -55,11 +60,25 @@ qed. record setoid1 : Type ≝ { carr1:> Type; eq1: carr1 → carr1 → CProp; - refl1: reflexive ? eq1; - sym1: symmetric ? eq1; - trans1: transitive ? eq1 + refl1: reflexive1 ? eq1; + sym1: symmetric1 ? eq1; + trans1: transitive1 ? eq1 }. +definition proofs1: CProp → setoid1. + intro; + constructor 1; + [ apply A + | intros; + apply True + | intro; + constructor 1 + | intros 3; + constructor 1 + | intros 5; + constructor 1] +qed. + definition CCProp: setoid1. constructor 1; [ apply CProp @@ -86,17 +105,16 @@ record function_space (A,B: setoid): Type ≝ }. notation "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Imply $a $b }. -interpretation "function_space" 'Imply a b = (function_space a b). record function_space1 (A: setoid1) (B: setoid1): Type ≝ { f1:1> A → B; - f1_ok: ∀a,a':A. proofs (eq1 ? a a') → proofs (eq1 ? (f1 a) (f1 a')) + f1_ok: ∀a,a':A. proofs1 (eq1 ? a a') → proofs1 (eq1 ? (f1 a) (f1 a')) }. - + definition function_space_setoid: setoid → setoid → setoid. intros (A B); constructor 1; - [ apply (A ⇒ B); + [ apply (function_space A B); | intros; apply (∀a:A. proofs (eq ? (f a) (f1 a))); | simplify; @@ -116,16 +134,14 @@ definition function_space_setoid: setoid → setoid → setoid. [ apply (f a) | apply (f1 a)]] qed. - -interpretation "function_space_setoid" 'Imply a b = (function_space_setoid a b). -definition function_space_setoid1: setoid1 → setoid1 → setoid. +definition function_space_setoid1: setoid1 → setoid1 → setoid1. intros (A B); constructor 1; [ apply (function_space1 A B); | intros; - apply (∀a:A. proofs (eq1 ? (f a) (f1 a))); - | simplify; + apply (∀a:A. proofs1 (eq1 ? (f a) (f1 a))); + |*: cases daemon] (* simplify; intros; apply (f1_ok ? ? x); unfold proofs; simplify; @@ -140,20 +156,20 @@ definition function_space_setoid1: setoid1 → setoid1 → setoid. unfold carr; unfold proofs; simplify; apply (trans1 B ? (y a)); [ apply (f a) - | apply (f1 a)]] + | apply (f1 a)]] *) qed. +interpretation "function_space_setoid1" 'Imply a b = (function_space_setoid1 a b). + record isomorphism (A,B: setoid): Type ≝ - { map1:> A ⇒ B; - map2:> B ⇒ A; + { map1:> function_space_setoid A B; + map2:> function_space_setoid B A; inv1: ∀a:A. proofs (eq ? (map2 (map1 a)) a); inv2: ∀b:B. proofs (eq ? (map1 (map2 b)) b) }. interpretation "isomorphism" 'iff x y = (isomorphism x y). -axiom daemon: False. - definition setoids: setoid1. constructor 1; [ apply setoid; @@ -166,9 +182,9 @@ definition setoids: setoid1. |3,4: intros; simplify; - unfold carr; unfold proofs; simplify; + unfold proofs; simplify; apply refl;] - |*: elim daemon] + |*: cases daemon] qed. definition setoid1_of_setoid: setoid → setoid1. @@ -178,26 +194,22 @@ definition setoid1_of_setoid: setoid → setoid1. | apply (eq s) | apply (refl s) | apply (sym s) - | apply (trans s) - ] + | apply (trans s)] qed. coercion setoid1_of_setoid. (* -record dependent_product (A:setoid1) (B: function_space1 A setoids): Type ≝ +record dependent_product (A:setoid) (B: A ⇒ setoids): Type ≝ { dp:> ∀a:A.carr (B a); - dp_ok: ∀a,a':A. ∀p:proofs (eq1 ? a a'). proofs (eq1 ? (dp a) (map2 ?? (f1_ok A ? B ?? p) (dp a'))) - }. -*) + dp_ok: ∀a,a':A. ∀p:proofs1 (eq1 ? a a'). proofs1 (eq1 ? (dp a) (map2 ?? (f1_ok ?? B ?? p) (dp a'))) + }.*) -record forall (A:setoid) (B: function_space1 A CCProp): CProp ≝ - { fo:> ∀a:A.proofs (B a) - }. +record forall (A:setoid) (B: A ⇒ CCProp): CProp ≝ + { fo:> ∀a:A.proofs (B a) }. record subset (A: setoid) : CProp ≝ - { mem: function_space1 A CCProp - }. + { mem: A ⇒ CCProp }. definition ssubset: setoid → setoid1. intro; @@ -210,21 +222,39 @@ definition ssubset: setoid → setoid1. intro; assumption | simplify; - elim daemon - | elim daemon] + cases daemon + | cases daemon] qed. - -definition mmem: ∀A:setoid. function_space_setoid1 (ssubset A) (function_space_setoid1 A CCProp). + +definition mmem: ∀A:setoid. (ssubset A) ⇒ A ⇒ CCProp. intros; constructor 1; [ apply mem; | unfold function_space_setoid1; simplify; intros (b b'); change in ⊢ (? (? (?→? (? %)))) with (mem ? b a \liff mem ? b' a); - unfold proofs; simplify; intros; - unfold proofs in c; simplify in c; + unfold proofs1; simplify; intros; + unfold proofs1 in c; simplify in c; unfold ssubset in c; simplify in c; cases (c a); clear c; split; assumption] -qed. \ No newline at end of file +qed. + +(* +definition sand: CCProp ⇒ CCProp. + +definition intersection: ∀A. ssubset A ⇒ ssubset A ⇒ ssubset A. + intro; + constructor 1; + [ intro; + constructor 1; + [ intro; + constructor 1; + constructor 1; + intro; + apply (mem ? c c2 ∧ mem ? c1 c2); + | + | + | +*)