X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Flib%2Fpts_dummy_new%2Farity.ma;fp=matita%2Fmatita%2Flib%2Fpts_dummy_new%2Farity.ma;h=3df7811c060e003335a8f36fb3dc3ac0badfc7cc;hb=46e87acb755894f9234191d675eeb5db4f5b930b;hp=0000000000000000000000000000000000000000;hpb=f8bc120b39bd74ade4e11d4d3ef4355f66c42495;p=helm.git

diff --git a/matita/matita/lib/pts_dummy_new/arity.ma b/matita/matita/lib/pts_dummy_new/arity.ma
new file mode 100644
index 000000000..3df7811c0
--- /dev/null
+++ b/matita/matita/lib/pts_dummy_new/arity.ma
@@ -0,0 +1,220 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "lambda/ext.ma".
+
+(* ARITIES ********************************************************************)
+
+(* An arity is a normal term representing the functional structure of a term.
+ * Arities can be freely applied as lon as the result is typable in λ→.
+ * we encode an arity with a family of meta-linguistic functions typed by λ→
+ * Such a family contains one member for each type of λ→ 
+ *)
+
+(* type of arity members ******************************************************)
+
+(* the type of an arity member *)
+inductive MEM: Type[0] ≝
+   | TOP: MEM
+   | FUN: MEM → MEM → MEM
+.
+
+definition pred ≝ λC. match C with
+   [ TOP     ⇒ TOP
+   | FUN _ A ⇒ A
+   ].
+
+definition decidable_MEq: ∀C1,C2:MEM. (C1 = C2) + (C1 ≠ C2).
+#C1 (elim C1) -C1
+   [ #C2 elim C2 -C2
+     [ /2/
+     | #B2 #A2 #_ #_ @inr @nmk #false destruct
+     ]
+   | #B1 #A1 #IHB1 #IHA1 #C2 elim C2 -C2
+     [ @inr @nmk #false destruct
+     | #B2 #A2 #_ #_ elim (IHB1 B2) -IHB1 #HB
+       [ elim (IHA1 A2) - IHA1 #HA
+         [ /2/ | @inr @nmk #false destruct elim HA /2/ ]
+       | @inr @nmk #false destruct elim HB /2/
+   ]
+qed.
+
+lemma fun_neq_sym: ∀A,C,B. pred C ≠ A → C ≠ FUN B A.
+#A #C #B #HA elim HA -HA #HA @nmk #H @HA -HA >H //
+qed. 
+
+(* arity members **************************************************************)
+
+(* the arity members of type TOP *)
+inductive Top: Type[0] ≝
+   | SORT: Top
+. 
+
+(* the arity members of type A *)
+let rec Mem A ≝ match A with
+   [ TOP     ⇒ Top
+   | FUN B A ⇒ Mem B → Mem A
+   ].
+
+(* the members of the arity "sort" *)
+let rec sort_mem A ≝ match A return λA. Mem A with
+   [ TOP     ⇒ SORT
+   | FUN B A ⇒ λ_.sort_mem A
+   ]. 
+
+(* arities ********************************************************************)
+
+(* the type of arities *)
+definition Arity ≝ ∀A. Mem A.
+
+(* the arity "sort" *)
+definition sort ≝ λA. sort_mem A.
+
+(* the arity "constant" *)
+definition const: ∀B. Mem B → Arity.
+#B #x #A. elim (decidable_MEq B A) #H [ elim H @x | @(sort_mem A) ]
+qed.
+
+(* application of arities *)
+definition aapp: MEM → Arity → Arity → Arity  ≝ λB,a,b,C. a (FUN B C) (b B).
+
+(* abstraction of arities *)
+definition aabst: (Arity → Arity) → Arity ≝
+   λf,C. match C return λC. Mem C with
+   [ TOP     ⇒ sort_mem TOP
+   | FUN B A ⇒ λx. f (const B x) A
+   ].
+
+(* extensional equality of arity members **************************************)
+
+(* Extensional equality of arity members (extensional equalty of functions).
+ * The functions may not respect extensional equality so reflexivity fails
+ * in general but may hold for specific arity members.
+ *)
+let rec ameq A ≝ match A return λA. Mem A → Mem A → Prop with
+   [ TOP     ⇒ λa1,a2. a1 = a2
+   | FUN B A ⇒ λa1,a2. ∀b1,b2. ameq B b1 b2 → ameq A (a1 b1) (a2 b2)
+   ].
+
+interpretation
+   "extensional equality (arity member)"
+   'Eq1 A a1 a2 = (ameq A a1 a2).
+
+(* reflexivity of extensional equality for an arity member *)
+definition invariant_mem ≝ λA,m. m ≅^A m.
+
+interpretation
+   "invariance (arity member)"
+   'Invariant1 a A = (invariant_mem A a).
+
+
+interpretation
+   "invariance (arity member with implicit type)"
+   'Invariant a = (invariant_mem ? a).
+
+lemma symmetric_ameq: ∀A. symmetric ? (ameq A).
+#A elim A -A /4/
+qed.
+
+lemma transitive_ameq: ∀A. transitive ? (ameq A).
+#A elim A -A /5/
+qed.
+
+lemma invariant_sort_mem: ∀A. ! sort_mem A.
+#A elim A normalize //
+qed.
+
+axiom const_eq: ∀A,x. const A x A ≅^A x.
+
+axiom const_neq: ∀A,B,x. A ≠ B → const A x B ≅^B (sort_mem B).
+
+(* extensional equality of arities ********************************************)
+
+definition aeq: Arity → Arity → Prop ≝ λa1,a2. ∀A. a1 A ≅^A a2 A.
+
+interpretation
+   "extensional equality (arity)"
+   'Eq a1 a2 = (aeq a1 a2).
+
+definition invariant: Arity → Prop ≝ λa. a ≅ a.
+
+interpretation
+   "invariance (arity)"
+   'Invariant a = (invariant a).
+
+lemma symmetric_aeq: symmetric … aeq.
+/2/ qed.
+
+lemma transitive_aeq: transitive … aeq.
+/2/ qed.
+
+lemma const_comp: ∀A,x1,x2. x1 ≅^A x2 → const … x1 ≅ const … x2.
+#A #x1 #x2 #Hx #C elim (decidable_MEq A C) #H
+   [ <H @transitive_ameq; [2: @const_eq | skip ]
+        @transitive_ameq; [2: @Hx | skip ]
+        @symmetric_ameq //
+   | @transitive_ameq; [2: @(const_neq … H) | skip ]
+     @transitive_ameq; [2: @invariant_sort_mem | skip ]
+     @symmetric_ameq /2/
+   ]
+qed.
+
+lemma aapp_comp: ∀C,a1,a2,b1,b2. a1 ≅ a2 → b1 ≅ b2 → aapp C a1 b1 ≅ aapp C a2 b2.
+#C #a1 #a2 #b1 #b2 #Ha #Hb #D @(Ha (FUN C D)) //
+qed.
+
+lemma aabst_comp: ∀f1,f2. (∀a1,a2. a1 ≅ a2 → f1 a1 ≅ f2 a2) →
+                  aabst f1 ≅ aabst f2.
+#f1 #f2 #H #C elim C -C // #B #A #_ #_ #b1 #b2 #Hb @H /2/
+qed.
+
+lemma invariant_sort: ! sort.
+normalize //
+qed.
+
+(* "is a constant arity" *)
+definition isc ≝ λa,A. const ? (a A) ≅ a.
+
+lemma isc_sort: ∀A. isc sort A.
+#A #C elim (decidable_MEq A C) #H [ <H // | /2 by const_neq/ ].
+qed.
+
+lemma isc_aapp: ∀B,A,b,a. ! b B → isc a A → isc (aapp B a b) (pred A).
+#B #A #b #a #Hb #Ha #C elim (decidable_MEq (pred A) C) #H [ >H // ]
+@transitive_ameq; [2: @(const_neq … H) | skip ]
+lapply (transitive_ameq ????? (Ha (FUN B C))) -Ha [3: #Ha @Ha // |2: skip ]
+@symmetric_ameq @const_neq /2/
+qed.
+
+(* extensional equality of arity contexts *************************************)
+
+definition aceq ≝ λE1,E2. all2 … aeq E1 E2.
+
+interpretation
+   "extensional equality (arity context)"
+   'Eq E1 E2 = (aceq E1 E2).
+
+definition invariant_env: list Arity → Prop ≝ λE. E ≅ E.
+
+interpretation
+   "invariance (arity context)"
+   'Invariant E = (invariant_env E).
+
+lemma symmetric_aceq: symmetric … aceq.
+/2/ qed.
+
+lemma nth_sort_comp: ∀E1,E2. E1 ≅ E2 →
+                     ∀i. nth i ? E1 sort ≅ nth i ? E2 sort.
+#E1 #E2 #H #i @(all2_nth … aeq) //
+qed.