From 54551ce5acf37f04972291e774d14371a671a8c7 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 22 Jul 2008 07:01:46 +0000 Subject: [PATCH] Sambin's & Valentini's toolbox (???) --- helm/software/matita/library/demo/toolbox.ma | 174 +++++++++++++++++++ 1 file changed, 174 insertions(+) create mode 100644 helm/software/matita/library/demo/toolbox.ma diff --git a/helm/software/matita/library/demo/toolbox.ma b/helm/software/matita/library/demo/toolbox.ma new file mode 100644 index 000000000..81ed8b065 --- /dev/null +++ b/helm/software/matita/library/demo/toolbox.ma @@ -0,0 +1,174 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "logic/cprop_connectives.ma". + +record iff (A,B: CProp) : CProp ≝ + { if: A → B; + fi: B → A + }. + +notation > "hvbox(a break \liff b)" + left associative with precedence 25 +for @{ 'iff $a $b }. + +notation "hvbox(a break \leftrightarrow b)" + left associative with precedence 25 +for @{ 'iff $a $b }. + +interpretation "logical iff" 'iff x y = (iff x y). + +record setoid : Type ≝ + { carr:> Type; + eq: carr → carr → CProp; + refl: reflexive ? eq; + sym: symmetric ? eq; + trans: transitive ? eq + }. + +definition proofs: CProp → setoid. + intro; + constructor 1; + [ apply A + | intros; + alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)". + apply True + | intro; + constructor 1 + | intros 3; + constructor 1 + | intros 5; + constructor 1] +qed. + +record setoid1 : Type ≝ + { carr1:> Type; + eq1: carr1 → carr1 → CProp; + refl1: reflexive ? eq1; + sym1: symmetric ? eq1; + trans1: transitive ? eq1 + }. + +definition CCProp: setoid1. + constructor 1; + [ apply CProp + | apply iff + | intro; + split; + intro; + assumption + | intros 3; + cases H; clear H; + split; + assumption + | intros 5; + cases H; cases H1; clear H H1; + split; + intros; + [ apply (H4 (H2 H)) + | apply (H3 (H5 H))]] +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') + }. + +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 ≝ + { f1:1> A → B; + f1_ok: ∀a,a':A. eq ? a a' → eq1 ? (f1 a) (f1 a') + }. + +definition function_space_setoid: setoid → setoid → setoid. + intros (A B); + constructor 1; + [ apply (A ⇒ B); + | intros; + apply (∀a:A. eq ? (f a) (f1 a)); + | simplify; + intros; + apply (f_ok ? ? x); + apply (refl A) + | simplify; + intros; + apply (sym B); + apply (H a) + | simplify; + intros; + apply (trans B ? (y a)); + [ apply (H a) + | apply (H1 a)]] +qed. + +interpretation "function_space_setoid" 'Imply a b = (function_space_setoid 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 + }. + +interpretation "isomorphism" 'iff x y = (isomorphism x y). + +axiom daemon: False. + +definition setoids: setoid1. + constructor 1; + [ apply setoid; + | apply isomorphism; + | intro; + split; + [1,2: constructor 1; + [1,3: intro; assumption; + |*: intros; assumption] + |3,4: + intros; + simplify; + apply refl;] + |*: elim daemon] +qed. + +record dependent_product (A:setoid) (B: function_space1 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')) + }. + +record forall (A:setoid) (B: function_space1 A CCProp): Type ≝ + { 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. + +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)); + assumption + | apply H3; clear H2 H3; + apply (fi ?? (f1_ok ?? (mem ? V) ?? H)); + apply H4;] +qed. + -- 2.39.2