From e1d6716c5560b046e0a7d0d871cc01a64cb31ca8 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Wed, 12 May 2010 18:41:47 +0000 Subject: [PATCH] Library support files for John Major equality and Russell. --- .../matita/nlibrary/Plogic/equality.ma | 8 +- helm/software/matita/nlibrary/Plogic/jmeq.ma | 37 ++++++++ .../matita/nlibrary/Plogic/russell_support.ma | 86 +++++++++++++++++++ 3 files changed, 130 insertions(+), 1 deletion(-) create mode 100644 helm/software/matita/nlibrary/Plogic/jmeq.ma create mode 100644 helm/software/matita/nlibrary/Plogic/russell_support.ma diff --git a/helm/software/matita/nlibrary/Plogic/equality.ma b/helm/software/matita/nlibrary/Plogic/equality.ma index 68e7aa509..a5972e270 100644 --- a/helm/software/matita/nlibrary/Plogic/equality.ma +++ b/helm/software/matita/nlibrary/Plogic/equality.ma @@ -29,6 +29,12 @@ nlemma eq_ind_r : #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r ? ? ? p0); nassumption. nqed. +nlemma eq_rect_Type2_r : + ∀A:Type.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p. + #A;#a;#P;#H;#x;#p;ngeneralize in match H;ngeneralize in match P; + ncases p;//; +nqed. + (* nlemma eq_ind_r : ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl_eq A a) → ∀x.∀p:eq ? x a.P x p. @@ -134,4 +140,4 @@ napply (R3 ????????? e0 ? e1 ? e2); napply a4; nqed. -naxiom streicherK : ∀T:Type[0].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p. \ No newline at end of file +naxiom streicherK : ∀T:Type[2].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p. \ No newline at end of file diff --git a/helm/software/matita/nlibrary/Plogic/jmeq.ma b/helm/software/matita/nlibrary/Plogic/jmeq.ma new file mode 100644 index 000000000..07105c616 --- /dev/null +++ b/helm/software/matita/nlibrary/Plogic/jmeq.ma @@ -0,0 +1,37 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "Plogic/equality.ma". + +(* experimental: JMeq support *) + +ninductive jmeq (A:Type[2]) (a:A) : ∀B:Type[2].B → Prop ≝ +| refl_jmeq : jmeq A a A a. + +naxiom jmeq_to_eq : ∀A:Type[2].∀a,b:A.jmeq A a A b → a = b. + +ncoercion jmeq_to_eq : ∀A:Type[2].∀a,b:A.∀p:jmeq A a A b.a = b ≝ + jmeq_to_eq on _p: jmeq ???? to eq ???. + +notation > "hvbox(a break ≃ b)" + non associative with precedence 45 +for @{ 'jmeq ? $a ? $b }. + +notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)" + non associative with precedence 45 +for @{ 'jmeq $t $a $u $b }. + +interpretation "john major's equality" 'jmeq t x u y = (jmeq t x u y). + +naxiom streicherKjmeq : ∀T:Type[2].∀t:T.∀P:t ≃ t → Type[2].P (refl_jmeq ? t) → ∀p.P p. \ No newline at end of file diff --git a/helm/software/matita/nlibrary/Plogic/russell_support.ma b/helm/software/matita/nlibrary/Plogic/russell_support.ma new file mode 100644 index 000000000..14273c98e --- /dev/null +++ b/helm/software/matita/nlibrary/Plogic/russell_support.ma @@ -0,0 +1,86 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "Plogic/jmeq.ma". +include "logic/connectives.ma". +include "datatypes/sums.ma". + +include "Plogic/connectives.ma". + +(* experimental: Russell support *) + +alias id "False" = "cic:/matita/ng/Plogic/connectives/False.ind(1,0,0)". + +ndefinition P_to_P_option : ∀A:Type[0].∀P:A → CProp[0].option A → CProp[0] ≝ + λA,P,a.match a with [ None ⇒ False | Some y ⇒ P y ]. + +ndefinition subset : ∀A:Type[0].(A → CProp[0]) → Type[0] ≝ + λA,P.Σx.P_to_P_option A P x. + +notation < "hvbox({ ident i : s | term 19 p })" with precedence 90 +for @{ 'subset_spec $s (\lambda ${ident i} : $nonexistent . $p)}. + +notation > "hvbox({ ident i : s | term 19 p })" with precedence 90 +for @{ 'subset_spec $s (\lambda ${ident i}. $p)}. + +(* + * the advantage is that we can use None to mean that some branch of the + * function we are defining will never be reached + * for all other purposes, they are the same as sigma types + * + * TODO: add on-the-fly rewriting for dependent types + *) +interpretation "russell-style subset specification" 'subset_spec s p = (subset s p). + +ndefinition inject : ∀A.∀P:A → CProp[0].∀a.∀p:P_to_P_option ? P a.{ x : A | P x } ≝ + λA.λP:A → CProp[0].λa:option A.λp:P_to_P_option ? P a. + sig_intro (option A) (P_to_P_option A P) a p. +ndefinition eject : ∀A.∀P: A → CProp[0].{ x : A | P x } → A ≝ + λA,P,c.match c with [ sig_intro w p ⇒ ?]. +ngeneralize in match p;ncases w;nnormalize +##[* +##|#x;#_;napply x ##] +nqed. + +ncoercion inject : + ∀A.∀P:A → CProp[0].∀a.∀p:P_to_P_option ? P a.subset ? (λx.P x) ≝ inject + on a:option ? to subset ? ?. +ncoercion eject : ∀A.∀P:A → CProp[0].∀c:subset ? P.A ≝ eject + on _c:subset ? ? to ?. + +(* +(* tests...*) + +include "datatypes/list.ma". + +ndefinition head : ∀l.l ≠ [] → { x : nat | ∃l2.l = x::l2 } ≝ + λl,p.match l with + [ nil ⇒ None ? + | cons x tl ⇒ Some ? x ].nnormalize; +##[ncases p;/3/ +##|/2/ +##] +nqed. + +ninductive vec : nat → Type[0] ≝ +| vnil : vec O +| vcons : ∀n:nat.nat → vec n → vec (S n). + +ndefinition vtail : + ∀n.∀v:vec (S n). { w : vec (pred (S n)) | ∃m:nat.v ≃ vcons ? m w } ≝ +λn,v.match v with + [ vnil ⇒ None (vec (pred O)) + | vcons p hd tl ⇒ Some (vec (pred (S p))) tl ]. +nnormalize;ndestruct;/2/; +nqed.*) \ No newline at end of file -- 2.39.2