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=81ed8b065a310f7222576da87c87259a1e08e2eb;hpb=54551ce5acf37f04972291e774d14371a671a8c7;p=helm.git diff --git a/helm/software/matita/library/demo/toolbox.ma b/helm/software/matita/library/demo/toolbox.ma index 81ed8b065..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 @@ -82,51 +101,75 @@ qed. record function_space (A,B: setoid): Type ≝ { f:1> A → B; - f_ok: ∀a,a':A. eq ? a a' → eq ? (f a) (f a') + f_ok: ∀a,a':A. proofs (eq ? a a') → proofs (eq ? (f a) (f a')) }. 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: setoid) (B: setoid1): Type ≝ +record function_space1 (A: setoid1) (B: setoid1): Type ≝ { f1:1> A → B; - f1_ok: ∀a,a':A. eq ? a a' → 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. eq ? (f a) (f1 a)); + apply (∀a:A. proofs (eq ? (f a) (f1 a))); | simplify; intros; apply (f_ok ? ? x); + unfold carr; unfold proofs; simplify; apply (refl A) | simplify; intros; + unfold carr; unfold proofs; simplify; apply (sym B); - apply (H a) + apply (f a) | simplify; intros; + unfold carr; unfold proofs; simplify; apply (trans B ? (y a)); - [ apply (H a) - | apply (H1 a)]] + [ apply (f a) + | apply (f1 a)]] +qed. + +definition function_space_setoid1: setoid1 → setoid1 → setoid1. + intros (A B); + constructor 1; + [ apply (function_space1 A B); + | intros; + apply (∀a:A. proofs1 (eq1 ? (f a) (f1 a))); + |*: cases daemon] (* simplify; + intros; + apply (f1_ok ? ? x); + unfold proofs; simplify; + apply (refl1 A) + | simplify; + intros; + unfold proofs; simplify; + apply (sym1 B); + apply (f a) + | simplify; + intros; + unfold carr; unfold proofs; simplify; + apply (trans1 B ? (y a)); + [ apply (f a) + | apply (f1 a)]] *) qed. - -interpretation "function_space_setoid" 'Imply a b = (function_space_setoid a b). + +interpretation "function_space_setoid1" 'Imply a b = (function_space_setoid1 a b). record isomorphism (A,B: setoid): Type ≝ - { map1:> A ⇒ B; - map2:> B ⇒ A; - inv1: ∀a:A. eq ? (map2 (map1 a)) a; - inv2: ∀b:B. eq ? (map1 (map2 b)) b + { 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; @@ -139,36 +182,79 @@ definition setoids: setoid1. |3,4: intros; simplify; + unfold proofs; simplify; apply refl;] - |*: elim daemon] + |*: cases daemon] qed. -record dependent_product (A:setoid) (B: function_space1 A setoids): Type ≝ +definition setoid1_of_setoid: setoid → setoid1. + intro; + constructor 1; + [ apply (carr s) + | apply (eq s) + | apply (refl s) + | apply (sym s) + | apply (trans s)] +qed. + +coercion setoid1_of_setoid. + +(* +record dependent_product (A:setoid) (B: A ⇒ setoids): Type ≝ { dp:> ∀a:A.carr (B a); - dp_ok: ∀a,a':A. ∀p:eq ? a a'. eq ? (dp a) (map2 ?? (f1_ok ?? 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): Type ≝ - { fo:> ∀a:A.proofs (B a) - }. +record forall (A:setoid) (B: A ⇒ CCProp): CProp ≝ + { fo:> ∀a:A.proofs (B a) }. -record subset (A: setoid) : Type ≝ - { mem: function_space1 A CCProp - }. - -definition subset_eq ≝ λA:setoid.λU,V: subset A. ∀a:A. mem ? U a \liff mem ? V a. +record subset (A: setoid) : CProp ≝ + { mem: A ⇒ CCProp }. -lemma mem_ok: - ∀A:setoid.∀a,a':A.∀U,V: subset A. - eq ? a a' → subset_eq ? U V → mem ? U a \liff mem ? V a'. - intros; - cases (H1 a); - split; intro H4; - [ lapply (H2 H4); clear H2 H3 H4; - apply (if ?? (f1_ok ?? (mem ? V) ?? H)); +definition ssubset: setoid → setoid1. + intro; + constructor 1; + [ apply (subset s); + | apply (λU,V:subset s. ∀a. mem ? U a \liff mem ? V a) + | simplify; + intros; + split; + intro; assumption - | apply H3; clear H2 H3; - apply (fi ?? (f1_ok ?? (mem ? V) ?? H)); - apply H4;] + | simplify; + cases daemon + | cases daemon] +qed. + +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 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. - + +(* +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); + | + | + | +*)