--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
+*)
(* 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 *)
].
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).
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 *)
∀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 →
∀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
].
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
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.
projects / helm.git / commitdiff