(* *)
(**************************************************************************)
-include "degree.ma".
-
+include "pts_dummy/degree.ma".
+(*
(* TO BE PUT ELSEWERE *)
lemma cons_append_assoc: ∀A,a. ∀l1,l2:list A. (a::l1) @ l2 = a :: (l1 @ l2).
// qed.
].
interpretation "CC2FO: K interpretation (context)" 'IK G = (KI G).
+*)
(* *)
(**************************************************************************)
-include "CC2FO_K.ma".
-include "cube.ma".
-include "inversion.ma".
-
+include "pts_dummy/CC2FO_K.ma".
+include "pts_dummy/cube.ma".
+include "pts_dummy/inversion.ma".
+(*
(* The K interpretation in the λ-Cube *****************************************)
lemma ki_type: ∀G,t,u. G ⊢_{CC} t : u → u = Sort 1 → 𝕂{G} ⊢_{FO} 𝕂{t}_[G] : u.
#G #t #u #H elim H -H G t u
[ #i #j * #_ @ax //
-| #G #A #i #HA #IHA #Heq
\ No newline at end of file
+| #G #A #i #HA #IHA #Heq
+*)
(* *)
(**************************************************************************)
-include "lambda/ext.ma".
-
+include "pts_dummy/ext.ma".
+(*
(* ARITIES ********************************************************************)
(* An arity is a normal term representing the functional structure of a term.
∀i. nth i ? E1 sort ≅ nth i ? E2 sort.
#E1 #E2 #H #i @(all2_nth … aeq) //
qed.
+*)
(* *)
(**************************************************************************)
-include "lambda/arity.ma".
-
+include "pts_dummy/arity.ma".
+(*
(* ARITY ASSIGNMENT ***********************************************************)
(* the arity type *************************************************************)
axiom pippo: ∀A:Type[0]. ∀a,b,c. (a::b) @ c = a :: b @ c.
@A qed.
*)
+*)
\ /
V_______________________________________________________________ *)
-include "lambda/reduction.ma".
-
+include "pts_dummy/reduction.ma".
+(*
(*
inductive T : Type[0] ≝
| Sort: nat → T
|@(ex_intro … M) @(ex_intro … M) % // % //
]
*)
+*)
(* *)
(**************************************************************************)
-include "convertibility.ma".
-include "types.ma".
-
+include "pts_dummy/convertibility.ma".
+include "pts_dummy/types.ma".
+(*
(* PURE TYPE SYSTEMS OF THE λ-CUBE ********************************************)
inductive Cube_Ax: nat → nat → Prop ≝
.
definition FO: pts ≝ mk_pts Cube_Ax FO_Re conv.
+*)
(* *)
(**************************************************************************)
-include "lambda/ext_lambda.ma".
-
+include "pts_dummy/ext_lambda.ma".
+(*
(* DEGREE ASSIGNMENT **********************************************************)
(* The degree of a term *******************************************************)
>append_Deg >append_Deg <Hvw -Hvw >DegHd_Lift; [2: //]
>deg_lift; [2,3: >HGk /2/] <(deg_subst … k) // >HGk /2/
qed.
+*)
(* *)
(**************************************************************************)
-include "basics/list.ma".
+include "basics/lists/list.ma".
(* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************)
(* *)
(**************************************************************************)
-include "lambda/ext.ma".
-include "lambda/subst.ma".
-
+include "pts_dummy/ext.ma".
+include "pts_dummy/subst.ma".
+(*
(* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************)
(* substitution ***************************************************************)
lemma tsubst_sort: ∀n,l. (Sort n)[/l] = Sort n.
// qed.
+*)
\ /
V_______________________________________________________________ *)
-include "lambda/types.ma".
-
+include "pts_dummy/types.ma".
+(*
(*
inductive TJ (p: pts): list T → T → T → Prop ≝
| ax : ∀i,j. Ax p i j → TJ p (nil T) (Sort i) (Sort j)
]
qed.
+*)
\ /
V_______________________________________________________________ *)
-include "lambda/terms.ma".
+include "pts_dummy/terms.ma".
+
+(* to be put elsewhere *)
+definition if_then_else ≝ λT:Type[0].λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
(* arguments: k is the depth (starts from 0), p is the height (starts from 0) *)
let rec lift t k p ≝
interpretation "Lift" 'Lift n k M = (lift M k n).
(*** properties of lift ***)
-
+(* BEGIN HERE
lemma lift_0: ∀t:T.∀k. lift t k 0 = t.
#t (elim t) normalize // #n #k cases (leb (S n) k) normalize //
qed.
lemma Lift_length: ∀p,G. |Lift G p| = |G|.
#p #G elim G -G; normalize //
qed.
+*)
\ No newline at end of file
\ /
V_______________________________________________________________ *)
-include "lambda/subterms.ma".
-
+include "pts_dummy/subterms.ma".
+(*
(*
inductive T : Type[0] ≝
| Sort: nat → T
#P #Q #R #pr1 #pr2 @(ex_intro … (full P)) /3/
qed.
+*)
(* *)
(**************************************************************************)
-include "lambda/rc_hsat.ma".
-
+include "pts_dummy/rc_hsat.ma".
+(*
(* THE EVALUATION *************************************************************)
(* The arity of a term t in an environment E *)
(a :: l1) @ l2 = a :: (l1 @ l2).
// qed.
*)
+
(* *)
(**************************************************************************)
-include "lambda/rc_sat.ma".
-
+include "pts_dummy/rc_sat.ma".
+(*
(* HIGHER ORDER REDUCIBILITY CANDIDATES ***************************************)
(* An arity is a type of λ→ to be used as carrier for a h.o. r.c. *)
lemma reflexive_defHRC: ∀P. defHRC P ≅^P defHRC P.
#P (elim P) -P (normalize) /2/
qed.
+*)
(* *)
(**************************************************************************)
-include "lambda/sn.ma".
-
+include "pts_dummy/sn.ma".
+(*
(* REDUCIBILITY CANDIDATES ****************************************************)
(* The reducibility candidate (r.c.) ******************************************)
definition lorRC: RC → RC → RC ≝ λB,C. mk_RC (lor_mem B C) ….
/2/ qed.
+*)
\ /
V_______________________________________________________________ *)
-include "lambda/par_reduction.ma".
+include "pts_dummy/par_reduction.ma".
include "basics/star.ma".
-
+(*
(*
inductive T : Type[0] ≝
| Sort: nat → T
@red_subst1 //
]
qed.
-
-
-
-
+*)
(* *)
(**************************************************************************)
-include "lambda/ext_lambda.ma".
-
+include "pts_dummy/ext_lambda.ma".
+(*
(* STRONGLY NORMALIZING TERMS *************************************************)
(* SN(t) holds when t is strongly normalizing *)
axiom sn_prod: ∀N,M. SN N → SN M → SN (Prod N M).
axiom sn_inv_app_1: ∀M,N. SN (App M N) → SN M.
+*)
\ /
V_______________________________________________________________ *)
-include "lambda/reduction.ma".
-include "lambda/inversion.ma".
-
+include "pts_dummy/reduction.ma".
+include "pts_dummy/inversion.ma".
+(*
(*
inductive T : Type[0] ≝
| Sort: nat → T
]
qed.
+*)
\ /
V_______________________________________________________________ *)
-include "lambda/lift.ma".
-
+include "pts_dummy/lift.ma".
+(*
let rec subst t k a ≝
match t with
[ Sort n ⇒ Sort n
(A [i ≝ B]) [i+k ≝ C] = (A [i+k+1 := C]) [i ≝ B [k ≝ C]].
#A #B #C #k #i >commutative_plus >subst_lemma //
qed.
+*)
\ /
V_______________________________________________________________ *)
-include "lambda/subst.ma".
-
+include "pts_dummy/subst.ma".
+(*
inductive subterm : T → T → Prop ≝
| appl : ∀M,N. subterm M (App M N)
| appr : ∀M,N. subterm N (App M N)
#N #M #subH (elim subH) normalize //
#M1 #N1 #P #sub1 #sub2 #size1 #size2 @(transitive_lt … size1 size2)
qed.
+*)
\ /
V_______________________________________________________________ *)
-include "basics/list.ma".
-include "lambda/lambda_notation.ma".
+include "basics/lists/list.ma".
+include "pts_dummy/lambda_notation.ma".
inductive T : Type[0] ≝
| Sort: nat → T (* starts from 0 *)
].
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 normalize //
qed.
(*
\ /
V_______________________________________________________________ *)
-include "lambda/subst.ma".
-include "basics/list.ma".
-
+include "pts_dummy/subst.ma".
+include "basics/lists/list.ma".
+(*
(*************************** substl *****************************)
let rec substl (G:list T) (N:T) : list T ≝
#P #G #v #w #Hv #t #u #Ht
lapply (substitution_tj … Ht ? ([]) … Hv) normalize //
qed.
+*)
(* *)
(**************************************************************************)
-include "lambda/ext.ma".
-
+include "pts_dummy/ext.ma".
+(*
(* ARITIES ********************************************************************)
(* An arity is a normal term representing the functional structure of a term.
∀i. nth i ? E1 sort ≅ nth i ? E2 sort.
#E1 #E2 #H #i @(all2_nth … aeq) //
qed.
+*)
(* *)
(**************************************************************************)
-include "lambda/arity.ma".
-
+include "pts_dummy/arity.ma".
+(*
(* ARITY ASSIGNMENT ***********************************************************)
(* the arity type *************************************************************)
axiom pippo: ∀A:Type[0]. ∀a,b,c. (a::b) @ c = a :: b @ c.
@A qed.
*)
+*)
\ /
V_______________________________________________________________ *)
-include "lambda/reduction.ma".
-
+include "pts_dummy/reduction.ma".
+(*
(*
inductive T : Type[0] ≝
| Sort: nat → T
|@(ex_intro … M) @(ex_intro … M) % // % //
]
*)
+*)
\ No newline at end of file
(* *)
(**************************************************************************)
-include "convertibility.ma".
-include "types.ma".
-
+include "pts_dummy/convertibility.ma".
+include "pts_dummy/types.ma".
+(*
(* PURE TYPE SYSTEMS OF THE λ-CUBE ********************************************)
inductive Cube_Ax: nat → nat → Prop ≝
.
definition FO: pts ≝ mk_pts Cube_Ax FO_Re conv.
+*)
(* *)
(**************************************************************************)
-include "basics/list.ma".
+include "basics/lists/list.ma".
(* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************)
(* *)
(**************************************************************************)
-include "lambda/ext.ma".
-include "lambda/subst.ma".
-
+include "pts_dummy/ext.ma".
+include "pts_dummy/subst.ma".
+(*
(* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************)
(* substitution ***************************************************************)
lemma tsubst_sort: ∀n,l. (Sort n)[/l] = Sort n.
// qed.
+*)
\ /
V_______________________________________________________________ *)
-include "lambdaN/thinning.ma".
+include "pts_dummy_new/thinning.ma".
(*
inductive TJ (p: pts): list T → T → T → Prop ≝
\ /
V_______________________________________________________________ *)
-include "lambdaN/subterms.ma".
+include "pts_dummy_new/subterms.ma".
(*
inductive T : Type[0] ≝
@(ex_intro … M2) @(ex_intro … N2) /3/
]
qed.
-
+(* BEGIN HERE
lemma prApp_not_lambda:
∀M,N,P. pr (App M N) P → is_lambda M = false →
∃M1,N1. (P = App M1 N1 ∧ pr M M1 ∧ pr N N1).
pr Q S ∧ pr P S.
#P #Q #R #pr1 #pr2 @(ex_intro … (full P)) /3/
qed.
-
+*)
(* *)
(**************************************************************************)
-include "lambda/rc_hsat.ma".
-
+include "pts_dummy/rc_hsat.ma".
+(*
(* THE EVALUATION *************************************************************)
(* The arity of a term t in an environment E *)
(* *)
(**************************************************************************)
-include "lambda/rc_sat.ma".
-
+include "pts_dummy/rc_sat.ma".
+(*
(* HIGHER ORDER REDUCIBILITY CANDIDATES ***************************************)
(* An arity is a type of λ→ to be used as carrier for a h.o. r.c. *)
lemma reflexive_defHRC: ∀P. defHRC P ≅^P defHRC P.
#P (elim P) -P (normalize) /2/
qed.
+*)
(* *)
(**************************************************************************)
-include "lambda/sn.ma".
-
+include "pts_dummy/sn.ma".
+(*
(* REDUCIBILITY CANDIDATES ****************************************************)
(* The reducibility candidate (r.c.) ******************************************)
definition lorRC: RC → RC → RC ≝ λB,C. mk_RC (lor_mem B C) ….
/2/ qed.
+*)
\ /
V_______________________________________________________________ *)
-include "lambdaN/par_reduction.ma".
+include "pts_dummy_new/par_reduction.ma".
include "basics/star.ma".
(*
definition reduct ≝ λn,m. red m n.
-definition SN ≝ WF ? reduct.
+definition SN : T → Prop ≝ WF ? reduct.
-definition NF ≝ λM. ∀N. ¬ (reduct N M).
+definition NF : T → Prop ≝ λM. ∀N. ¬ (reduct N M).
theorem NF_to_SN: ∀M. NF M → SN M.
#M #nfM % #a #red @False_ind /2/
lemma star_appl: ∀M,M1,N. star … red M M1 →
star … red (App M N) (App M1 N).
#M #M1 #N #star1 (elim star1) //
-#B #C #starMB #redBC #H @(inj … H) /2/
+#B #C #starMB #redBC #H /3 width=3/
qed.
lemma star_appr: ∀M,N,N1. star … red N N1 →
star … red (App M N) (App M N1).
#M #N #N1 #star1 (elim star1) //
-#B #C #starMB #redBC #H @(inj … H) /2/
+#B #C #starMB #redBC #H /3 width=3/
qed.
lemma star_app: ∀M,M1,N,N1. star … red M M1 → star … red N N1 →
lemma star_laml: ∀M,M1,N. star … red M M1 →
star … red (Lambda M N) (Lambda M1 N).
#M #M1 #N #star1 (elim star1) //
-#B #C #starMB #redBC #H @(inj … H) /2/
+#B #C #starMB #redBC #H /3 width=3/
qed.
lemma star_lamr: ∀M,N,N1. star … red N N1 →
star … red (Lambda M N) (Lambda M N1).
#M #N #N1 #star1 (elim star1) //
-#B #C #starMB #redBC #H @(inj … H) /2/
+#B #C #starMB #redBC #H /3 width=3/
qed.
lemma star_lam: ∀M,M1,N,N1. star … red M M1 → star … red N N1 →
lemma star_prodl: ∀M,M1,N. star … red M M1 →
star … red (Prod M N) (Prod M1 N).
#M #M1 #N #star1 (elim star1) //
-#B #C #starMB #redBC #H @(inj … H) /2/
+#B #C #starMB #redBC #H /3 width=3/
qed.
lemma star_prodr: ∀M,N,N1. star … red N N1 →
star … red (Prod M N) (Prod M N1).
#M #N #N1 #star1 (elim star1) //
-#B #C #starMB #redBC #H @(inj … H) /2/
+#B #C #starMB #redBC #H /3 width=3/
qed.
lemma star_prod: ∀M,M1,N,N1. star … red M M1 → star … red N N1 →
lemma star_dl: ∀M,M1,N. star … red M M1 →
star … red (D M N) (D M1 N).
#M #M1 #N #star1 (elim star1) //
-#B #C #starMB #redBC #H @(inj … H) /2/
+#B #C #starMB #redBC #H /3 width=3/
qed.
lemma star_dr: ∀M,N,N1. star … red N N1 →
star … red (D M N) (D M N1).
#M #N #N1 #star1 (elim star1) //
-#B #C #starMB #redBC #H @(inj … H) /2/
+#B #C #starMB #redBC #H /3 width=3/
qed.
lemma star_d: ∀M,M1,N,N1. star … red M M1 → star … red N N1 →
#P #snP (elim snP) #A #snA #HindA
#N #snN (elim snN) #B #snB #HindB
#M #snM1 (cut (SH M)) [@SN_to_SH @(SN_subst … snM1)] #shM
-(generalize in match snM1) (elim shM)
-#C #shC #HindC #snC1 % #Q #redQ (cases (red_app … redQ))
+generalize in match snM1; elim shM
+#C #shC #HindC #snC1 % #Q #redQ cases (red_app … redQ);
[*
[* #M2 * #N2 * #eqlam destruct #eqQ //
|* #M2 * #eqQ #redlam >eqQ (cases (red_lambda …redlam))
(* *)
(**************************************************************************)
-include "lambda/ext_lambda.ma".
-
+include "pts_dummy/ext_lambda.ma".
+(*
(* STRONGLY NORMALIZING TERMS *************************************************)
(* SN(t) holds when t is strongly normalizing *)
axiom sn_prod: ∀N,M. SN N → SN M → SN (Prod N M).
axiom sn_inv_app_1: ∀M,N. SN (App M N) → SN M.
+*)
\ /
V_______________________________________________________________ *)
-include "lambdaN/reduction.ma".
-include "lambdaN/inversion.ma".
+include "pts_dummy_new/reduction.ma".
+include "pts_dummy_new/inversion.ma".
(*
inductive T : Type[0] ≝
|#G1 #A #i #t1 #_ #P @(ex_intro … i) @(weak … t1 t1)
|#G1 #A #B #C #i #t1 #t2 #H1 #H2 #H3 (cases (H1 ?) )
[#i #Bi @(ex_intro … i) @(weak … Bi t2)
- |#i @(not_to_not … (H3 i)) //
+ |#i @(not_to_not … (H3 i)) /2 width=2/
]
|#G1 #A #B #i #j #k #h #t1 #t2 #_ #_ #H3 @False_ind /2/
|#G1 #A #B #C #D #t1 #t2 #H1 #H2 #H3 cases (H1 ?);
\ /
V_______________________________________________________________ *)
-include "lambdaN/terms.ma".
+include "pts_dummy_new/terms.ma".
+
+(* to be put elsewhere *)
+definition if_then_else ≝ λT:Type[0].λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
(* arguments: k is the depth (starts from 0), p is the height (starts from 0) *)
let rec lift t k p ≝
lemma subst_lift_k: ∀A,B.∀k. (lift B k 1)[k ≝ A] = B.
#A #B (elim B) normalize /2/ #n #k
@(leb_elim k n) normalize #Hnk
- [cut (k ≤ n+1) [@transitive_le //] #H
+ [cut (k ≤ n+1); [@transitive_le //] #H
>(le_to_leb_true … H) normalize
>(not_eq_to_eqb_false k (n+1)) normalize /2/
|>(lt_to_leb_false … (not_le_to_lt … Hnk)) normalize //
[2,3,4,5: #T #T0 #Hind1 #Hind2 #i #j #k #leij #lejk
@eq_f2 /2/ @Hind2 (applyS (monotonic_le_plus_l 1)) //
|#n #i #j #k #leij #ltjk @(leb_elim i n) normalize #len
- [cut (j < n + S k)
+ [cut (j < n + S k);
[<plus_n_Sm @le_S_S @(transitive_le … ltjk) /2/] #H
>(le_to_leb_true j (n+S k));
[normalize >(not_eq_to_eqb_false j (n+S k)) normalize /2/
[cut (k+i+1 = n); [/2/] #H1
>(le_to_leb_true (k+i+1) n) /2/
>(eq_to_eqb_true … H1) normalize
- (generalize in match ltin)
+ generalize in match ltin;
@(lt_O_n_elim … posn) #m #leim >delift // /2/
|(cut (k+i < n-1)) [@not_eq_to_le_to_lt; //] #Hlt
>(le_to_leb_true (k+i+1) n);
\ /
V_______________________________________________________________ *)
-include "lambdaN/subst.ma".
+include "pts_dummy_new/subst.ma".
inductive subterm : T → T → Prop ≝
| appl : ∀M,N. subterm M (App M N)
\ /
V_______________________________________________________________ *)
-include "basics/list.ma".
-include "lambda/lambda_notation.ma".
+include "basics/lists/list.ma".
+include "pts_dummy/lambda_notation.ma".
inductive T : Type[0] ≝
| Sort: nat → T (* starts from 0 *)
\ /
V_______________________________________________________________ *)
-include "lambdaN/types.ma".
+include "pts_dummy_new/types.ma".
(*
inductive TJ (p: pts): list T → T → T → Prop ≝
#Heq1 <Heq1 @(Hind2 ? (P::D)) normalize //
]
|#G #P #Q #R #S #tjP #tjS #Hind1 #Hind2
- #G1 #D #A #l #Heq #tjA (normalize in Hind1 ⊢ %)
+ #G1 #D #A #l #Heq #tjA normalize in Hind1 ⊢ %;
>(lift_subst_up R S 1 0 (length ? D)) @(app … (lift Q (length ? D) 1));
[@Hind1 // |@Hind2 //]
|#G #P #Q #R #i #tjR #tjProd #Hind1 #Hind2
#G1 #D #A #l #Heq #tjA normalize @(abs … i);
[cut (∀n. S n = n +1); [//] #H <H
@(Hind1 G1 (P::D) … tjA) normalize //
- |(normalize in Hind2) @(Hind2 …tjA) //
+ | normalize in Hind2; @(Hind2 …tjA) //
]
|#G #P #Q #R #i #convQR #tjP #tjQ #Hind1 #Hind2
#G1 #D #A #l #Heq #tjA
\ /
V_______________________________________________________________ *)
-include "lambdaN/subst.ma".
-include "basics/list.ma".
+include "pts_dummy_new/subst.ma".
+include "basics/lists/list.ma".
(*************************** substl *****************************)
]
|#G #A1 #i #tjA #Hind #G1 #D (cases D)
[#N #Heq #tjN >(delift (lift N O O) A1 O O O ??) //
- (normalize in Heq) destruct /2/
- |#H #L #N1 #Heq (normalize in Heq)
+ normalize in Heq; destruct normalize /2/
+ |#H #L #N1 #Heq normalize in Heq;
#tjN1 normalize destruct; (applyS start) /2/
]
|#G #P #Q #R #i #tjP #tjR #Hind1 #Hind2 #G1 #D #N
#Heq1 <Heq1 @(Hind2 ? (P::D)) normalize //
]
|#G #P #Q #R #S #tjP #tjS #Hind1 #Hind2
- #G1 #D #N #Heq #tjN (normalize in Hind1 ⊢ %)
- >(plus_n_O (length ? D)) in ⊢ (? ? ? ? (? ? % ?))
- >(subst_lemma R S N ? 0) (applyS app) /2/
+ #G1 #D #N #Heq #tjN normalize in Hind1 ⊢ %;
+ >(plus_n_O (length ? D)) in ⊢ (? ? ? ? (? ? % ?));
+ >(subst_lemma R S N ? 0) applyS app /2/
|#G #P #Q #R #i #tjR #tjProd #Hind1 #Hind2
#G1 #D #N #Heq #tjN normalize
(applyS abs)
- [normalize in Hind2 /2/
+ [normalize in Hind2; /2/
|(* napplyS (Hind1 G1 (P::D) N ? tjN); sistemare *)
generalize in match (Hind1 G1 (P::D) N ? tjN);
- [#H (normalize in H) (applyS H) | normalize // ]
+ [#H normalize in H; applyS H | normalize // ]
]
|#G #P #Q #R #i #convQR #tjP #tjQ #Hind1 #Hind2
#G1 #D #N #Heq #tjN
We need to define the latter operations. The following flatten function takes in
input a list of words and concatenates them together. *)
-(* FG: flatten in list.ma gets in the way:
-alias id "flatten" = "cic:/matita/tutorial/chapter6/flatten.fix(0,1,4)".
-does not work, so we use flatten in lists for now
-
+(* Already in the library
let rec flatten (S : DeqSet) (l : list (word S)) on l : word S ≝
match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
*)
lemma cat_to_star:∀S.∀A:word S → Prop.
∀w1,w2. A w1 → A^* w2 → A^* (w1@w2).
#S #A #w1 #w2 #Aw * #l * #H #H1 @(ex_intro … (w1::l))
-% destruct // normalize /2/
+% normalize destruct /2/ (* destruct added *)
qed.
lemma fix_star: ∀S.∀A:word S → Prop.
[* #l generalize in match w; -w cases l [normalize #w * /2/]
#w1 #tl #w * whd in ⊢ ((??%?)→?); #eqw whd in ⊢ (%→?); *
#w1A #cw1 %1 @(ex_intro … w1) @(ex_intro … (flatten S tl))
- % destruct /2/ whd @(ex_intro … tl) /2/
+ % destruct /2/ whd @(ex_intro … tl) /2/ (* destruct added *)
|* [2: whd in ⊢ (%→?); #eqw <eqw //]
* #w1 * #w2 * * #eqw <eqw @cat_to_star
]
A^* ∪ {ϵ} =1 A^*.
#S #A #w % /2/ * //
qed.
-
\ No newline at end of file
+
| pc E1 E2 ⇒ (forget ? E1) · (forget ? E2)
| po E1 E2 ⇒ (forget ? E1) + (forget ? E2)
| pk E ⇒ (forget ? E)^* ].
-
+
+(* Already in the library
+notation "| term 19 C |" with precedence 70 for @{ 'card $C }.
+*)
interpretation "forget" 'card a = (forget ? a).
lemma erase_dot : ∀S.∀e1,e2:pitem S. |e1 · e2| = c ? (|e1|) (|e2|).
[/3/ | * * // #H1 #H2 @False_ind @(absurd …H1 H2)]
|>sem_pre_false normalize in ⊢ (??%?); #w % [ /3/ | * // ]
]
-qed.
\ No newline at end of file
+qed.
projects / helm.git / commitdiff