Library support files for John Major equality and Russell.

diff --git a/helm/software/matita/nlibrary/Plogic/equality.ma b/helm/software/matita/nlibrary/Plogic/equality.ma
index 68e7aa50917fae4e68e80d702b8bb89a3a035350..a5972e2709446cce6a401ba28c228e93920b54ac 100644 (file)
--- 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 (file)
index 0000000..07105c6
--- /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 (file)
index 0000000..14273c9
--- /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