From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 15 Mar 2011 19:18:39 +0000 (+0000)
Subject: - more notation and service lemmas
X-Git-Tag: make_still_working~2562
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7a490593a8c798ac35007ddcc61da3b9153ac619;p=helm.git

- more notation and service lemmas
- arity.ma: arities and arity types
- arity_eval.ma: arities and arity types assigned to terms
---

diff --git a/matita/matita/lib/lambda/arity.ma b/matita/matita/lib/lambda/arity.ma
new file mode 100644
index 000000000..3df7811c0
--- /dev/null
+++ b/matita/matita/lib/lambda/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.
diff --git a/matita/matita/lib/lambda/arity_eval.ma b/matita/matita/lib/lambda/arity_eval.ma
new file mode 100644
index 000000000..6fcf0e0c0
--- /dev/null
+++ b/matita/matita/lib/lambda/arity_eval.ma
@@ -0,0 +1,228 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/arity.ma".
+
+(* ARITY ASSIGNMENT ***********************************************************)
+
+(* the arity type *************************************************************)
+
+(* arity type assigned to the term t in the environment E *)
+let rec ata K t on t ≝  match t with
+   [ Sort _     ⇒ TOP
+   | Rel i      ⇒ nth i … K TOP
+   | App M N    ⇒ pred (ata K M) 
+   | Lambda N M ⇒ let C ≝ ata K N in FUN C (ata (C::K) M)
+   | Prod _ _   ⇒ TOP
+   | D M        ⇒ TOP (* ??? not so sure yet *)
+   ].
+
+interpretation "arity type assignment" 'IInt1 t K = (ata K t).
+
+lemma ata_app: ∀M,N,K. 〚App M N〛_[K] = pred (〚M〛_[K]).
+// qed.
+
+lemma ata_lambda: ∀M,N,K. 〚Lambda N M〛_[K] = FUN (〚N〛_[K]) (〚M〛_[〚N〛_[K]::K]).
+// qed.
+
+lemma ata_rel_lt: ∀H,K,i. (S i) ≤ |K| → 〚Rel i〛_[K @ H] = 〚Rel i〛_[K].
+#H #K elim K -K [1: #i #Hie elim (not_le_Sn_O i) #Hi elim (Hi Hie) ]
+#A #K #IHK #i elim i -i // #i #_ #Hie @IHK @le_S_S_to_le @Hie
+qed.
+
+lemma ata_rel_ge: ∀H,K,i. (S i) ≰ |K| →
+                  〚Rel i〛_[K @ H] = 〚Rel (i-|K|)〛_[H].
+#H #K elim K -K [ normalize // ]
+#A #K #IHK #i elim i -i [1: -IHK #Hie elim Hie -Hie #Hie; elim (Hie ?) /2/ ]
+normalize #i #_ #Hie @IHK /2/
+qed.
+
+(* weakeing and thinning lemma for the arity type assignment *)
+(* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
+lemma ata_lift: ∀p,K,Kp. p = |Kp| → ∀t,k,Kk. k = |Kk| →
+                〚lift t k p〛_[Kk @ Kp @ K] = 〚t〛_[Kk @ K].
+#p #K #Kp #HKp #t elim t -t //
+   [ #i #k #Kk #HKk @(leb_elim (S i) k) #Hik
+     [ >(lift_rel_lt … Hik) >HKk in Hik #Hik
+       >(ata_rel_lt … Hik) >(ata_rel_lt … Hik) //
+     | >(lift_rel_ge … Hik) >HKk in Hik #Hik
+       >(ata_rel_ge … Hik) <associative_append
+       >(ata_rel_ge …) >length_append >HKp;
+       [ >arith2 // @not_lt_to_le /2/ | @(arith3 … Hik) ]
+     ]
+   | #M #N #IHM #_ #k #Kk #HKk >lift_app >ata_app /3/
+   | #N #M #IHN #IHM #k #Kk #HKk >lift_lambda >ata_lambda
+     >IHN // >(IHM … (? :: ?)) // >commutative_plus /2/ 
+   ]
+qed.
+
+(* substitution lemma for the arity type assignment *)
+(* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
+lemma ata_subst: ∀v,K,t,k,Kk. k = |Kk| → 
+                 〚t[k≝v]〛_[Kk @ K] = 〚t〛_[Kk @ 〚v〛_[K]::K].
+#v #K #t elim t -t //
+   [ #i #k #Kk #HKk @(leb_elim (S i) k) #H1ik
+     [ >(subst_rel1 … H1ik) >HKk in H1ik #H1ik
+       >(ata_rel_lt … H1ik) >(ata_rel_lt … H1ik) //
+     | @(eqb_elim i k) #H2ik
+       [ >H2ik in H1ik -H2ik i #H1ik >subst_rel2 >HKk in H1ik #H1ik
+         >(ata_rel_ge … H1ik) <minus_n_n >(ata_lift ? ? ? ? ? ? ([])) //
+       | lapply (arith4 … H1ik H2ik) -H1ik H2ik #Hik >(subst_rel3 … Hik)
+          >ata_rel_ge; [2: /2/ ] <(associative_append ? ? ([?]) ?)
+           >ata_rel_ge >length_append >commutative_plus;
+           [ <minus_plus // | <HKk -HKk Kk @not_le_to_not_le_S_S /3/ ]
+       ]
+     ]
+   | #M #N #IHM #_ #k #Kk #HKk >subst_app >ata_app /3/
+   | #N #M #IHN #IHM #k #Kk #HKk >subst_lambda > ata_lambda
+     >IHN // >commutative_plus >(IHM … (? :: ?)) /2/
+   ]
+qed.
+
+(* the arity ******************************************************************)
+
+(* arity assigned to the term t in the environments E and K *)
+let rec aa K E t on t ≝ match t with
+   [ Sort _     ⇒ sort
+   | Rel i      ⇒ nth i … E sort
+   | App M N    ⇒ aapp (〚N〛_[K]) (aa K E M) (aa K E N)
+   | Lambda N M ⇒ aabst (λc. aa (〚N〛_[K]::K) (c :: E) M)
+   | Prod N M   ⇒ aabst (λc. aa (〚N〛_[K]::K) (c :: E) M)
+   | D M        ⇒ sort (* ??? not so sure yet *)
+   ].
+
+interpretation "arity assignment" 'IInt2 t E K = (aa K E t).
+
+lemma aa_app: ∀M,N,E,K. 〚App M N〛_[E,K] = aapp (〚N〛_[K]) (〚M〛_[E,K]) (〚N〛_[E,K]).
+// qed.
+
+lemma aa_lambda: ∀N,M,E,K. 〚Lambda N M〛_[E,K] = aabst (λc. 〚M〛_[c :: E, 〚N〛_[K]::K]).
+// qed.
+
+lemma aa_prod: ∀N,M,E,K. 〚Prod N M〛_[E,K] = aabst (λc. 〚M〛_[c :: E, 〚N〛_[K]::K]).
+// qed.
+
+lemma aa_rel_lt: ∀K2,K1,D,E,i. (S i) ≤ |E| →
+                 〚Rel i〛_[E @ D, K1] = 〚Rel i〛_[E, K2].
+#K1 #K1 #D #E elim E -E [1: #i #Hie elim (not_le_Sn_O i) #Hi elim (Hi Hie) ]
+#C #E #IHE #i elim i -i // #i #_ #Hie @IHE @le_S_S_to_le @Hie
+qed.
+
+lemma aa_rel_lt_id: ∀K,D,E,i. (S i) ≤ |E| →
+                    〚Rel i〛_[E @ D, K] = 〚Rel i〛_[E, K].
+#K @(aa_rel_lt K) qed.
+
+lemma aa_rel_ge: ∀K2,K1,D,E,i. (S i) ≰ |E| →
+                 〚Rel i〛_[E @ D, K1] = 〚Rel (i-|E|)〛_[D, K2].
+#K2 #K1 #D #E elim E -E [ normalize // ]
+#C #E #IHE #i elim i -i [1: -IHE #Hie elim Hie -Hie #Hie elim (Hie ?) /2/ ]
+normalize #i #_ #Hie @IHE /2/
+qed.
+
+lemma aa_rel_ge_id: ∀K,D,E,i. (S i) ≰ |E| →
+                    〚Rel i〛_[E @ D, K] = 〚Rel (i-|E|)〛_[D, K].
+#K @(aa_rel_ge K) qed.
+
+(* weakeing and thinning lemma for the arity assignment *)
+(* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
+lemma aa_lift: ∀K,E1,E2. E1 ≅ E2 → ∀p,Kp,Ep. p=|Kp| → p = |Ep| →
+               ∀t,k,Kk,E1k,E2k. k = |Kk| → k = |E1k| → E1k ≅ E2k →
+               〚lift t k p〛_[E1k @ Ep @ E1, Kk @ Kp @ K] ≅ 〚t〛_[E2k @ E2, Kk @ K].
+#K #E1 #E2 #HE #p #Kp #Ep #HKp #HEp #t elim t -t /2 by invariant_sort/
+   [ #i #k #Kk #E1k #E2k #HKk #HE1k #HEk @(leb_elim (S i) k) #Hik
+     [ >(lift_rel_lt … Hik) >HE1k in Hik #Hik >(aa_rel_lt_id … Hik)
+       >(all2_length … HEk) in Hik #Hik >(aa_rel_lt_id … Hik) /2 by nth_sort_comp/
+     | >(lift_rel_ge … Hik) >HE1k in Hik #Hik <(associative_append … E1k)
+       >(aa_rel_ge_id …) >length_append >HEp; [2: @(arith3 … Hik) ]
+       >(all2_length … HEk) in Hik #Hik >(aa_rel_ge_id … Hik) >arith2;
+       [ /2 by nth_sort_comp/ | @not_lt_to_le /2/ ]
+     ]
+   | #M #N #IHM #IHN #k #Kk #E1k #E2k #HKk #HE1k #HEk >lift_app >aa_app
+     >ata_lift /3/
+   | #N #M #_ #IHM #k #Kk #E1k #E2k #HKk #HE1k #HEk >lift_lambda >aa_lambda
+     @aabst_comp #a1 #a2 #Ha >ata_lift // >commutative_plus
+     @(IHM ? (?::?) (?::?) (?::?)); [ >HKk | >HE1k ] /2/
+   | #N #M #_ #IHM #k #Kk #E1k #E2k #HKk #HE1k #HEk >lift_prod >aa_prod
+     @aabst_comp #a1 #a2 #Ha >ata_lift // >commutative_plus
+     @(IHM ? (?::?) (?::?) (?::?)); [ >HKk | >HE1k ] /2/
+   ]
+qed.
+
+lemma aa_comp: ∀E1,E2. E1 ≅ E2 → ∀t,K. 〚t〛_[E1, K] ≅ 〚t〛_[E2, K].
+#E1 #E2 #HE #t #K <(lift_0 t 0) in ⊢ (? % ?)
+@(aa_lift … ([]) ([]) … ([]) ([]) ([])) //
+qed.
+
+(* the assigned arity is invariant *)
+lemma aa_invariant: ∀t,E,K. !E → !〚t〛_[E, K].
+/2/ qed.
+
+(* substitution lemma for the arity assignment *)
+(* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
+lemma aa_subst: ∀K,E1,E2. E1 ≅ E2 →
+                ∀v,t,k,Kk,E1k,E2k. k = |Kk| → k = |E1k| → E1k ≅ E2k →
+                〚t[k≝v]〛_[E1k@E1, Kk@K] ≅ 〚t〛_[E2k@〚v〛_[E2,K]::E2, Kk@〚v〛_[K]::K].
+#K #E1 #E2 #HE #v #t elim t -t /2 by invariant_sort/
+   [ #i #k #Kk #E1k #E2k #HKk #HE1k #HEk @(leb_elim (S i) k) #H1ik
+     [ >(subst_rel1 … H1ik) >HE1k in H1ik #H1ik >(aa_rel_lt_id … H1ik)
+       >(all2_length … HEk) in H1ik #H1ik >(aa_rel_lt_id … H1ik) /2/
+     | @(eqb_elim i k) #H2ik
+       [ >H2ik in H1ik -H2ik i #H1ik >subst_rel2 >HE1k in H1ik #H1ik
+         >(all2_length … HEk) in H1ik #H1ik >(aa_rel_ge_id … H1ik) <minus_n_n
+         >HE1k in HKk #HKk -HE1k k  >(all2_length … HEk) in HKk #HKk
+         @(aa_lift … ([]) ([]) ([])) /3/
+       | lapply (arith4 … H1ik H2ik) -H1ik H2ik #Hik
+         >(subst_rel3 … Hik) >aa_rel_ge_id; [2: /2/ ]
+         <(associative_append ? ? ([?]) ?) in ⊢ (? ? (? ? % ?))
+         >HE1k in Hik #Hik >(aa_rel_ge (Kk@K))
+         >length_append >commutative_plus <(all2_length … HEk);
+         [ <minus_plus /2/ | @not_le_to_not_le_S_S /3/ ]
+       ]
+     ]
+   | #M #N #IHM #IHN #k #Kk #E1k #E2k #HKk #HE1k #HEk >subst_app >aa_app
+     >ata_subst /3/
+   | #N #M #_ #IHM #k #Kk #E1k #E2k #HKk #HE1k #HEk >subst_lambda >aa_lambda
+     @aabst_comp #a1 #a2 #Ha >ata_subst // >commutative_plus
+     @(IHM ? (?::?) (?::?) (?::?)); [ >HKk | >HE1k ] /2/
+   | #N #M #_ #IHM #k #Kk #E1k #E2k #HKk #HE1k #HEk >subst_prod >aa_prod
+     @aabst_comp #a1 #a2 #Ha >ata_subst // >commutative_plus
+     @(IHM ? (?::?) (?::?) (?::?)); [ >HKk | >HE1k ] /2/
+   ]
+qed.
+
+(* the assigned arity is constant *)
+lemma aa_isc: ∀t,E,K. !E → all2 … isc E K → isc (〚t〛_[E,K]) (〚t〛_[K]).
+#t elim t -t /2 by isc_sort/
+   [ #i #E #K #HE #H @(all2_nth … isc) //
+   | /3/
+   | #N #M #IHN #IHM #E #K #HE #H >aa_lambda >ata_lambda 
+
+
+
+(*
+const ? (〚v〛_[E1,K] (〚v〛_[K])) ≅ 〚v〛_[E1,K].
+
+theorem aa_beta: ∀K,E1,E2. E1 ≅ E2 → ∀w,t,v. 〚v〛_[K] = 〚w〛_[K] →
+                 〚App (Lambda w t) v〛_[E1,K] ≅ 〚t[0≝v]〛_[E2,K].
+#K #E1 #E2 #HE #w #t #v #H > aa_app >aa_lambda
+@transitive_aeq; [3: @symmetric_aeq @(aa_subst … E1 … ([]) ([]) ([])) /2/ | skip ]
+>H @aa_comp -H v; #C whd in ⊢ (? ? % ?)
+*)
+
+(*
+axiom cons_comp: ∀a1,a2. a1 ≅ a2 → ∀E1,E2. E1 ≅ E2 → a1 :: E1 ≅ a2 :: E2.
+
+axiom pippo: ∀A:Type[0]. ∀a,b,c. (a::b) @ c = a :: b @ c.
+@A qed.
+*)
diff --git a/matita/matita/lib/lambda/ext.ma b/matita/matita/lib/lambda/ext.ma
index cd619adf5..2e2f30359 100644
--- a/matita/matita/lib/lambda/ext.ma
+++ b/matita/matita/lib/lambda/ext.ma
@@ -44,7 +44,7 @@ qed.
 (* lists **********************************************************************)
 
 lemma length_append: ∀A. ∀(l2,l1:list A). |l1@l2| = |l1| + |l2|.
-#A #l2 #l1 (elim l1) -l1 (normalize) //
+#A #l2 #l1 elim l1 -l1; normalize //
 qed.
 
 (* all(?,P,l) holds when P holds for all members of l *)
@@ -54,11 +54,11 @@ let rec all (A:Type[0]) (P:A→Prop) l on l ≝ match l with
    ].
 
 lemma all_hd: ∀A:Type[0]. ∀P:A→Prop. ∀a. P a → ∀l. all … P l → P (hd … l a).
-#A #P #a #Ha #l elim l -l [ #_ @Ha | #b #l #_ #Hl elim Hl // ]
+#A #P #a #Ha #l elim l -l [ #_ @Ha | #b #l #_ #Hl elim Hl -Hl // ]
 qed.
 
 lemma all_tl: ∀A:Type[0]. ∀P:A→Prop. ∀l. all … P l →  all … P (tail … l).
-#A #P #l elim l -l // #b #l #IH #Hl elim Hl //
+#A #P #l elim l -l // #b #l #IH #Hl elim Hl -Hl //
 qed.
 
 lemma all_nth: ∀A:Type[0]. ∀P:A→Prop. ∀a. P a → ∀i,l. all … P l → P (nth i … l a).
@@ -66,7 +66,7 @@ lemma all_nth: ∀A:Type[0]. ∀P:A→Prop. ∀a. P a → ∀i,l. all … P l 
 qed.
 
 lemma all_append: ∀A,P,l2,l1. all A P l1 → all A P l2 → all A P (l1 @ l2).
-#A #P #l2 #l1 (elim l1) -l1 (normalize) // #hd #tl #IH1 #H (elim H) /3/
+#A #P #l2 #l1 elim l1 -l1; normalize // #hd #tl #IH1 #H elim H -H /3/
 qed.
 
 (* all2(?,P,l1,l2) holds when P holds for all paired members of l1 and l2 *)
@@ -82,21 +82,21 @@ lemma all2_length: ∀A,B:Type[0]. ∀P:A→B→Prop.
                    ∀l1,l2. all2 … P l1 l2 → |l1|=|l2|.
 #A #B #P #l1 elim l1 -l1 [ #l2 #H >H // ]
 #x1 #l1 #IH1 #l2 elim l2 -l2 [ #false elim false ]
-#x2 #l2 #_ #H elim H normalize /3/
+#x2 #l2 #_ #H elim H -H; normalize /3/
 qed. 
 
 lemma all2_hd: ∀A,B:Type[0]. ∀P:A→B→Prop. ∀a,b. P a b →
                ∀l1,l2. all2 … P l1 l2 → P (hd … l1 a) (hd … l2 b).
 #A #B #P #a #b #Hab #l1 elim l1 -l1 [ #l2 #H2 >H2 @Hab ]
 #x1 #l1 #_ #l2 elim l2 -l2 [ #false elim false ]
-#x2 #l2 #_ #H elim H //
+#x2 #l2 #_ #H elim H -H //
 qed.
 
 lemma all2_tl: ∀A,B:Type[0]. ∀P:A→B→Prop.
                ∀l1,l2. all2 … P l1 l2 →  all2 … P (tail … l1) (tail … l2).
 #A #B #P #l1 elim l1 -l1 [ #l2 #H >H // ]
 #x1 #l1 #_ #l2 elim l2 -l2 [ #false elim false ]
-#x2 #l2 #_ #H elim H // 
+#x2 #l2 #_ #H elim H -H // 
 qed.
 
 lemma all2_nth: ∀A,B:Type[0]. ∀P:A→B→Prop. ∀a,b. P a b →
@@ -108,9 +108,15 @@ lemma all2_append: ∀A,B,P,l2,m2. all2 A B P l2 m2 →
                    ∀l1,m1. all2 A B P l1 m1 → all2 A B P (l1 @ l2) (m1 @ m2).
 #A #B #P #l2 #m2 #H2 #l1 (elim l1) -l1 [ #m1 #H >H @H2 ] 
 #x1 #l1 #IH1 #m2 elim m2 -m2 [ #false elim false ]
-#x2 #m2 #_ #H elim H /3/
+#x2 #m2 #_ #H elim H -H /3/
 qed.
 
+lemma all2_symmetric: ∀A. ∀P:A→A→Prop. symmetric … P → symmetric … (all2 … P).
+#A #P #HP #l1 elim l1 -l1 [ #l2 #H >H // ]
+#x1 #l1 #IH1 #l2 elim l2 -l2 [ #false elim false ]
+#x2 #l2 #_ #H elim H -H /3/
+qed.   
+
 (* terms **********************************************************************)
 
 (* Appl F l generalizes App applying F to a list of arguments
@@ -122,7 +128,7 @@ let rec Appl F l on l ≝ match l with
    ].
 
 lemma appl_append: ∀N,l,M. Appl M (l @ [N]) = App (Appl M l) N.
-#N #l (elim l) -l // #hd #tl #IHl #M >IHl //
+#N #l elim l -l // #hd #tl #IHl #M >IHl //
 qed.
 
 (* FG: not needed for now 
@@ -189,9 +195,8 @@ let rec tsubst M l on l ≝ match l with
 interpretation "telescopic substitution" 'Subst1 M l = (tsubst M l).
 
 lemma tsubst_refl: ∀l,t. (lift t 0 (|l|))[l] = t.
-#l (elim l) -l (normalize) // #hd #tl #IHl #t cut (S (|tl|) = |tl| + 1) // (**) (* eliminate cut *)
+#l elim l -l; normalize // #hd #tl #IHl #t cut (S (|tl|) = |tl| + 1) // (**) (* eliminate cut *)
 qed.
 
 lemma tsubst_sort: ∀n,l. (Sort n)[l] = Sort n.
-//
-qed.
+// qed.
diff --git a/matita/matita/lib/lambda/lambda_notation.ma b/matita/matita/lib/lambda/lambda_notation.ma
index 0ad437ab0..26185019a 100644
--- a/matita/matita/lib/lambda/lambda_notation.ma
+++ b/matita/matita/lib/lambda/lambda_notation.ma
@@ -14,7 +14,7 @@
 
 (* NOTATION FOR THE LAMBDA CALCULUS *******************************************)
 
-(* equivalences *)
+(* equivalence, invariance *)
 
 notation "hvbox(a break ≅ b)" 
   non associative with precedence 45
@@ -24,6 +24,14 @@ notation "hvbox(a break (≅ ^ term 90 c) b)"
   non associative with precedence 45
   for @{'Eq1 $c $a $b}.
 
+notation "hbox(! term 50 a)"
+  non associative with precedence 50
+  for @{'Invariant $a}.
+
+notation "hbox((! ^ term 90 b) term 50 a)"
+  non associative with precedence 50
+  for @{'Invariant1 $a $b}.
+
 (* lifting, substitution *)
 
 notation "hvbox(M break [ l ])"