(* Note: this is Tait's iii, or Girard's CR4 *)
definition S2 ≝ λRR:lenv→relation term. λRS:relation term. λRP,C:lenv→predicate term.
∀L,Vs. all … (RP L) Vs →
- â\88\80T. ð\9d\95\8a[T] → NF … (RR L) RS T → C L (ⒶVs.T).
+ â\88\80T. ð\9d\90\92[T] → NF … (RR L) RS T → C L (ⒶVs.T).
(* Note: this is Tait's ii *)
definition S3 ≝ λRP,C:lenv→predicate term.
(* Basic inversion lemmas ***************************************************)
-fact simple_inv_bind_aux: â\88\80T. ð\9d\95\8a[T] → ∀J,W,U. T = ⓑ{J} W. U → False.
+fact simple_inv_bind_aux: â\88\80T. ð\9d\90\92[T] → ∀J,W,U. T = ⓑ{J} W. U → False.
#T * -T
[ #I #J #W #U #H destruct
| #I #V #T #J #W #U #H destruct
]
qed.
-lemma simple_inv_bind: â\88\80I,V,T. ð\9d\95\8a[ⓑ{I} V. T] → False.
+lemma simple_inv_bind: â\88\80I,V,T. ð\9d\90\92[ⓑ{I} V. T] → False.
/2 width=6/ qed-.
inductive thom: relation term ≝
| thom_atom: ∀I. thom (⓪{I}) (⓪{I})
| thom_abst: ∀V1,V2,T1,T2. thom (ⓛV1. T1) (ⓛV2. T2)
- | thom_appl: â\88\80V1,V2,T1,T2. thom T1 T2 â\86\92 ð\9d\95\8a[T1] â\86\92 ð\9d\95\8a[T2] →
+ | thom_appl: â\88\80V1,V2,T1,T2. thom T1 T2 â\86\92 ð\9d\90\92[T1] â\86\92 ð\9d\90\92[T2] →
thom (ⓐV1. T1) (ⓐV2. T2)
.
lemma thom_refl1: ∀T1,T2. T1 ≈ T2 → T1 ≈ T1.
/3 width=2/ qed.
-lemma simple_thom_repl_dx: â\88\80T1,T2. T1 â\89\88 T2 â\86\92 ð\9d\95\8a[T1] â\86\92 ð\9d\95\8a[T2].
+lemma simple_thom_repl_dx: â\88\80T1,T2. T1 â\89\88 T2 â\86\92 ð\9d\90\92[T1] â\86\92 ð\9d\90\92[T2].
#T1 #T2 #H elim H -T1 -T2 //
#V1 #V2 #T1 #T2 #H
elim (simple_inv_bind … H)
qed. (**) (* remove from index *)
-lemma simple_thom_repl_sn: â\88\80T1,T2. T1 â\89\88 T2 â\86\92 ð\9d\95\8a[T2] â\86\92 ð\9d\95\8a[T1].
+lemma simple_thom_repl_sn: â\88\80T1,T2. T1 â\89\88 T2 â\86\92 ð\9d\90\92[T2] â\86\92 ð\9d\90\92[T1].
/3 width=3/ qed-.
(* Basic inversion lemmas ***************************************************)
/2 width=5/ qed-.
fact thom_inv_flat1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = ⓕ{I}W1.U1 →
- â\88\83â\88\83W2,U2. U1 â\89\88 U2 & ð\9d\95\8a[U1] & ð\9d\95\8a[U2] &
+ â\88\83â\88\83W2,U2. U1 â\89\88 U2 & ð\9d\90\92[U1] & ð\9d\90\92[U2] &
I = Appl & T2 = ⓐW2. U2.
#T1 #T2 * -T1 -T2
[ #J #I #W1 #U1 #H destruct
qed.
lemma thom_inv_flat1: ∀I,W1,U1,T2. ⓕ{I}W1.U1 ≈ T2 →
- â\88\83â\88\83W2,U2. U1 â\89\88 U2 & ð\9d\95\8a[U1] & ð\9d\95\8a[U2] &
+ â\88\83â\88\83W2,U2. U1 â\89\88 U2 & ð\9d\90\92[U1] & ð\9d\90\92[U2] &
I = Appl & T2 = ⓐW2. U2.
/2 width=4/ qed-.
non associative with precedence 90
for @{ 'Weight $x $y }.
-notation "hvbox( ð\9d\95\8a [ T ] )"
+notation "hvbox( ð\9d\90\92 [ T ] )"
non associative with precedence 45
for @{ 'Simple $T }.
(* Substitution *************************************************************)
+notation "hvbox( L ⊢ break [ d , break e ] break 𝐑 [ T ] )"
+ non associative with precedence 45
+ for @{ 'Reducible $L $d $e $T }.
+
+notation "hvbox( L ⊢ break [ d , break e ] break 𝐈 [ T ] )"
+ non associative with precedence 45
+ for @{ 'NotReducible $L $d $e $T }.
+
+notation "hvbox( L ⊢ break [ d , break e ] break 𝐍 [ T ] )"
+ non associative with precedence 45
+ for @{ 'Normal $L $d $e $T }.
+
notation "hvbox( ⇧ [ d , break e ] break T1 ≡ break T2 )"
non associative with precedence 45
for @{ 'RLift $d $e $T1 $T2 }.
(* Reducibility *************************************************************)
-notation "hvbox( ℝ [ T ] )"
+notation "hvbox( 𝐑 [ T ] )"
non associative with precedence 45
for @{ 'Reducible $T }.
-notation "hvbox( L ⊢ ℝ [ T ] )"
+notation "hvbox( L ⊢ break 𝐑 [ T ] )"
non associative with precedence 45
for @{ 'Reducible $L $T }.
-notation "hvbox( ð\9d\95\80 [ T ] )"
+notation "hvbox( ð\9d\90\88 [ T ] )"
non associative with precedence 45
for @{ 'NotReducible $T }.
-notation "hvbox( L ⊢ 𝕀 [ T ] )"
+notation "hvbox( L ⊢ break 𝐈 [ T ] )"
non associative with precedence 45
for @{ 'NotReducible $L $T }.
-notation "hvbox( ℕ [ T ] )"
+notation "hvbox( 𝐍 [ T ] )"
non associative with precedence 45
for @{ 'Normal $T }.
-notation "hvbox( L ⊢ ℕ [ T ] )"
+notation "hvbox( L ⊢ break 𝐍 [ T ] )"
non associative with precedence 45
for @{ 'Normal $L $T }.
-notation "hvbox( ð\9d\95\8eâ\84\8dâ\84\9d [ T ] )"
+notation "hvbox( ð\9d\90\96ð\9d\90\87ð\9d\90\91 [ T ] )"
non associative with precedence 45
for @{ 'WHdReducible $T }.
-notation "hvbox( L ⊢ 𝕎ℍℝ [ T ] )"
+notation "hvbox( L ⊢ break 𝐖𝐇𝐑 [ T ] )"
non associative with precedence 45
for @{ 'WHdReducible $L $T }.
-notation "hvbox( ð\9d\95\8eâ\84\8dð\9d\95\80 [ T ] )"
+notation "hvbox( ð\9d\90\96ð\9d\90\87ð\9d\90\88 [ T ] )"
non associative with precedence 45
for @{ 'NotWHdReducible $T }.
-notation "hvbox( L ⊢ 𝕎ℍ𝕀 [ T ] )"
+notation "hvbox( L ⊢ break 𝐖𝐇𝐈 [ T ] )"
non associative with precedence 45
for @{ 'NotWHdReducible $L $T }.
-notation "hvbox( ð\9d\95\8eâ\84\8dâ\84\95 [ T ] )"
+notation "hvbox( ð\9d\90\96ð\9d\90\87ð\9d\90\8d [ T ] )"
non associative with precedence 45
for @{ 'WHdNormal $T }.
-notation "hvbox( L ⊢ 𝕎ℍℕ [ T ] )"
+notation "hvbox( L ⊢ break 𝐖𝐇𝐍 [ T ] )"
non associative with precedence 45
for @{ 'WHdNormal $L $T }.
--- /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 "Basic_2/reducibility/trf.ma".
+
+(* CONTEXT-FREE IRREDUCIBLE TERMS *******************************************)
+
+definition tif: predicate term ≝ λT. 𝐑[T] → False.
+
+interpretation "context-free irreducibility (term)"
+ 'NotReducible T = (tif T).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma tif_inv_abbr: ∀V,T. 𝐈[ⓓV.T] → False.
+/2 width=1/ qed-.
+
+lemma tif_inv_abst: ∀V,T. 𝐈[ⓛV.T] → 𝐈[V] ∧ 𝐈[T].
+/4 width=1/ qed-.
+
+lemma tif_inv_appl: ∀V,T. 𝐈[ⓐV.T] → ∧∧ 𝐈[V] & 𝐈[T] & 𝐒[T].
+#V #T #HVT @and3_intro /3 width=1/
+generalize in match HVT; -HVT elim T -T //
+* // * #U #T #_ #_ #H elim (H ?) -H /2 width=1/
+qed-.
+
+lemma tif_inv_cast: ∀V,T. 𝐈[ⓣV.T] → False.
+/2 width=1/ qed-.
+
+(* Basic properties *********************************************************)
+
+lemma tif_atom: ∀I. 𝐈[⓪{I}].
+/2 width=4/ qed.
+
+lemma tif_abst: ∀V,T. 𝐈[V] → 𝐈[T] → 𝐈[ⓛV.T].
+#V #T #HV #HT #H
+elim (trf_inv_abst … H) -H /2 width=1/
+qed.
+
+lemma tif_appl: ∀V,T. 𝐈[V] → 𝐈[T] → 𝐒[T] → 𝐈[ⓐV.T].
+#V #T #HV #HT #S #H
+elim (trf_inv_appl … H) -H /2 width=1/
+qed.
(* Basic inversion lemmas ***************************************************)
-lemma tnf_inv_abst: ∀V,T. ℕ[ⓛV.T] → ℕ[V] ∧ ℕ[T].
+lemma tnf_inv_abst: ∀V,T. 𝐍[ⓛV.T] → 𝐍[V] ∧ 𝐍[T].
#V1 #T1 #HVT1 @conj
[ #V2 #HV2 lapply (HVT1 (ⓛV2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct //
| #T2 #HT2 lapply (HVT1 (ⓛV1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //
]
qed-.
-lemma tnf_inv_appl: ∀V,T. ℕ[ⓐV.T] → ∧∧ ℕ[V] & ℕ[T] & 𝕊[T].
+lemma tnf_inv_appl: ∀V,T. 𝐍[ⓐV.T] → ∧∧ 𝐍[V] & 𝐍[T] & 𝐒[T].
#V1 #T1 #HVT1 @and3_intro
[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct //
| #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //
]
qed-.
-lemma tnf_inv_abbr: ∀V,T. ℕ[ⓓV.T] → False.
+lemma tnf_inv_abbr: ∀V,T. 𝐍[ⓓV.T] → False.
#V #T #H elim (is_lift_dec T 0 1)
[ * #U #HTU
lapply (H U ?) -H /2 width=3/ #H destruct
]
qed.
-lemma tnf_inv_cast: ∀V,T. ℕ[ⓣV.T] → False.
+lemma tnf_inv_cast: ∀V,T. 𝐍[ⓣV.T] → False.
#V #T #H lapply (H T ?) -H /2 width=1/ #H
@(discr_tpair_xy_y … H)
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 "Basic_2/substitution/tps_lift.ma".
+include "Basic_2/reducibility/tif.ma".
+include "Basic_2/reducibility/tnf.ma".
+
+(* CONTEXT-FREE NORMAL TERMS ************************************************)
+
+(* Main properties properties ***********************************************)
+
+lemma tpr_tif_eq: ∀T1,T2. T1 ➡ T2 → 𝐈[T1] → T1 = T2.
+#T1 #T2 #H elim H -T1 -T2
+[ //
+| * #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H
+ [ elim (tif_inv_appl … H) -H #HV1 #HT1 #_
+ >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 //
+ | elim (tif_inv_cast … H)
+ ]
+| #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H
+ elim (tif_inv_appl … H) -H #_ #_ #H
+ elim (simple_inv_bind … H)
+| * #V1 #V2 #T1 #T #T2 #_ #_ #HT2 #IHV1 #IHT1 #H
+ [ -HT2 -IHV1 -IHT1 elim (tif_inv_abbr … H)
+ | <(tps_inv_refl_SO2 … HT2 ?) -HT2 //
+ elim (tif_inv_abst … H) -H #HV1 #HT1
+ >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 //
+ ]
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H
+ elim (tif_inv_appl … H) -H #_ #_ #H
+ elim (simple_inv_bind … H)
+| #V1 #T1 #T2 #T #_ #_ #_ #H
+ elim (tif_inv_abbr … H)
+| #V1 #T1 #T #_ #_ #H
+ elim (tif_inv_cast … H)
+]
+qed.
+
+theorem tif_tnf: ∀T1. 𝐈[T1] → 𝐍[T1].
+/2 width=1/ qed.
+
+(* Note: this property is unusual *)
+lemma tnf_trf_false: ∀T1. 𝐑[T1] → 𝐍[T1] → False.
+#T1 #H elim H -T1
+[ #V #T #_ #IHV #H elim (tnf_inv_abst … H) -H /2 width=1/
+| #V #T #_ #IHT #H elim (tnf_inv_abst … H) -H /2 width=1/
+| #V #T #_ #IHV #H elim (tnf_inv_appl … H) -H /2 width=1/
+| #V #T #_ #IHV #H elim (tnf_inv_appl … H) -H /2 width=1/
+| #V #T #H elim (tnf_inv_abbr … H)
+| #V #T #H elim (tnf_inv_cast … H)
+| #V #W #T #H elim (tnf_inv_appl … H) -H #_ #_ #H
+ elim (simple_inv_bind … H)
+]
+qed.
+
+theorem tnf_tif: ∀T1. 𝐍[T1] → 𝐈[T1].
+/2 width=3/ qed.
+
+lemma tnf_abst: ∀V,T. 𝐍[V] → 𝐍[T] → 𝐍[ⓛV.T].
+/4 width=1/ qed.
+
+lemma tnf_appl: ∀V,T. 𝐍[V] → 𝐍[T] → 𝐒[T] → 𝐍[ⓐV.T].
+/4 width=1/ 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 "Basic_2/substitution/tps_lift.ma".
-include "Basic_2/reducibility/trf.ma".
-include "Basic_2/reducibility/tnf.ma".
-
-(* CONTEXT-FREE NORMAL TERMS ************************************************)
-
-(* Main properties properties ***********************************************)
-
-lemma tpr_tif_eq: ∀T1,T2. T1 ➡ T2 → 𝕀[T1] → T1 = T2.
-#T1 #T2 #H elim H -T1 -T2
-[ //
-| * #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H
- [ elim (tif_inv_appl … H) -H #HV1 #HT1 #_
- >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 //
- | elim (tif_inv_cast … H)
- ]
-| #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H
- elim (tif_inv_appl … H) -H #_ #_ #H
- elim (simple_inv_bind … H)
-| * #V1 #V2 #T1 #T #T2 #_ #_ #HT2 #IHV1 #IHT1 #H
- [ -HT2 -IHV1 -IHT1 elim (tif_inv_abbr … H)
- | <(tps_inv_refl_SO2 … HT2 ?) -HT2 //
- elim (tif_inv_abst … H) -H #HV1 #HT1
- >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 //
- ]
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H
- elim (tif_inv_appl … H) -H #_ #_ #H
- elim (simple_inv_bind … H)
-| #V1 #T1 #T2 #T #_ #_ #_ #H
- elim (tif_inv_abbr … H)
-| #V1 #T1 #T #_ #_ #H
- elim (tif_inv_cast … H)
-]
-qed.
-
-theorem tif_tnf: ∀T1. 𝕀[T1] → ℕ[T1].
-/2 width=1/ qed.
-
-(* Note: this property is unusual *)
-lemma tnf_trf_false: ∀T1. ℝ[T1] → ℕ[T1] → False.
-#T1 #H elim H -T1
-[ #V #T #_ #IHV #H elim (tnf_inv_abst … H) -H /2 width=1/
-| #V #T #_ #IHT #H elim (tnf_inv_abst … H) -H /2 width=1/
-| #V #T #_ #IHV #H elim (tnf_inv_appl … H) -H /2 width=1/
-| #V #T #_ #IHV #H elim (tnf_inv_appl … H) -H /2 width=1/
-| #V #T #H elim (tnf_inv_abbr … H)
-| #V #T #H elim (tnf_inv_cast … H)
-| #V #W #T #H elim (tnf_inv_appl … H) -H #_ #_ #H
- elim (simple_inv_bind … H)
-]
-qed.
-
-theorem tnf_tif: ∀T1. ℕ[T1] → 𝕀[T1].
-/2 width=3/ qed.
-
-lemma tnf_abst: ∀V,T. ℕ[V] → ℕ[T] → ℕ[ⓛV.T].
-/4 width=1/ qed.
-
-lemma tnf_appl: ∀V,T. ℕ[V] → ℕ[T] → 𝕊[T] → ℕ[ⓐV.T].
-/4 width=1/ qed.
qed-.
(* Note: the main property of simple terms *)
-lemma tpr_inv_appl1_simple: â\88\80V1,T1,U. â\93\90V1. T1 â\9e¡ U â\86\92 ð\9d\95\8a[T1] →
+lemma tpr_inv_appl1_simple: â\88\80V1,T1,U. â\93\90V1. T1 â\9e¡ U â\86\92 ð\9d\90\92[T1] →
∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 &
U = ⓐV2. T2.
#V1 #T1 #U #H #HT1
include "Basic_2/grammar/term_simple.ma".
-(* CONTEXT-FREE REDUCIBLE AND IRREDUCIBLE TERMS *****************************)
+(* CONTEXT-FREE REDUCIBLE TERMS *********************************************)
(* reducible terms *)
inductive trf: predicate term ≝
"context-free reducibility (term)"
'Reducible T = (trf T).
-(* irreducible terms *)
-definition tif: predicate term ≝ λT. ℝ[T] → False.
-
-interpretation
- "context-free irreducibility (term)"
- 'NotReducible T = (tif T).
-
(* Basic inversion lemmas ***************************************************)
-fact trf_inv_atom_aux: ∀I,T. ℝ[T] → T = ⓪{I} → False.
+fact trf_inv_atom_aux: ∀I,T. 𝐑[T] → T = ⓪{I} → False.
#I #T * -T
[ #V #T #_ #H destruct
| #V #T #_ #H destruct
]
qed.
-lemma trf_inv_atom: ∀I. ℝ[⓪{I}] → False.
+lemma trf_inv_atom: ∀I. 𝐑[⓪{I}] → False.
/2 width=4/ qed-.
-fact trf_inv_abst_aux: ∀W,U,T. ℝ[T] → T = ⓛW. U → ℝ[W] ∨ ℝ[U].
+fact trf_inv_abst_aux: ∀W,U,T. 𝐑[T] → T = ⓛW. U → 𝐑[W] ∨ 𝐑[U].
#W #U #T * -T
[ #V #T #HV #H destruct /2 width=1/
| #V #T #HT #H destruct /2 width=1/
]
qed.
-lemma trf_inv_abst: ∀V,T. ℝ[ⓛV.T] → ℝ[V] ∨ ℝ[T].
+lemma trf_inv_abst: ∀V,T. 𝐑[ⓛV.T] → 𝐑[V] ∨ 𝐑[T].
/2 width=3/ qed-.
-fact trf_inv_appl_aux: ∀W,U,T. ℝ[T] → T = ⓐW. U →
- ∨∨ ℝ[W] | ℝ[U] | (𝕊[U] → False).
+fact trf_inv_appl_aux: ∀W,U,T. 𝐑[T] → T = ⓐW. U →
+ ∨∨ 𝐑[W] | 𝐑[U] | (𝐒[U] → False).
#W #U #T * -T
[ #V #T #_ #H destruct
| #V #T #_ #H destruct
]
qed.
-lemma trf_inv_appl: ∀W,U. ℝ[ⓐW.U] → ∨∨ ℝ[W] | ℝ[U] | (𝕊[U] → False).
+lemma trf_inv_appl: ∀W,U. 𝐑[ⓐW.U] → ∨∨ 𝐑[W] | 𝐑[U] | (𝐒[U] → False).
/2 width=3/ qed-.
-
-lemma tif_inv_abbr: ∀V,T. 𝕀[ⓓV.T] → False.
-/2 width=1/ qed-.
-
-lemma tif_inv_abst: ∀V,T. 𝕀[ⓛV.T] → 𝕀[V] ∧ 𝕀[T].
-/4 width=1/ qed-.
-
-lemma tif_inv_appl: ∀V,T. 𝕀[ⓐV.T] → ∧∧ 𝕀[V] & 𝕀[T] & 𝕊[T].
-#V #T #HVT @and3_intro /3 width=1/
-generalize in match HVT; -HVT elim T -T //
-* // * #U #T #_ #_ #H elim (H ?) -H /2 width=1/
-qed-.
-
-lemma tif_inv_cast: ∀V,T. 𝕀[ⓣV.T] → False.
-/2 width=1/ qed-.
-
-(* Basic properties *********************************************************)
-
-lemma tif_atom: ∀I. 𝕀[⓪{I}].
-/2 width=4/ qed.
-
-lemma tif_abst: ∀V,T. 𝕀[V] → 𝕀[T] → 𝕀[ⓛV.T].
-#V #T #HV #HT #H
-elim (trf_inv_abst … H) -H /2 width=1/
-qed.
-
-lemma tif_appl: ∀V,T. 𝕀[V] → 𝕀[T] → 𝕊[T] → 𝕀[ⓐV.T].
-#V #T #HV #HT #S #H
-elim (trf_inv_appl … H) -H /2 width=1/
-qed.
(* Basic inversion lemmas ***************************************************)
-lemma twhnf_inv_thom: â\88\80T. ð\9d\95\8eâ\84\8dâ\84\95[T] → T ≈ T.
+lemma twhnf_inv_thom: â\88\80T. ð\9d\90\96ð\9d\90\87ð\9d\90\8d[T] → T ≈ T.
normalize /2 width=1/
qed-.
]
qed.
-lemma twhnf_thom: â\88\80T. T â\89\88 T â\86\92 ð\9d\95\8eâ\84\8dâ\84\95[T].
+lemma twhnf_thom: â\88\80T. T â\89\88 T â\86\92 ð\9d\90\96ð\9d\90\87ð\9d\90\8d[T].
/2 width=1/ qed.
#d #e #T1 #T2 #H elim H -d -e -T1 -T2 normalize //
qed-.
-lemma lift_simple_dx: â\88\80d,e,T1,T2. â\87§[d, e] T1 â\89¡ T2 â\86\92 ð\9d\95\8a[T1] â\86\92 ð\9d\95\8a[T2].
+lemma lift_simple_dx: â\88\80d,e,T1,T2. â\87§[d, e] T1 â\89¡ T2 â\86\92 ð\9d\90\92[T1] â\86\92 ð\9d\90\92[T2].
#d #e #T1 #T2 #H elim H -d -e -T1 -T2 //
#I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #H
elim (simple_inv_bind … H)
qed-.
-lemma lift_simple_sn: â\88\80d,e,T1,T2. â\87§[d, e] T1 â\89¡ T2 â\86\92 ð\9d\95\8a[T2] â\86\92 ð\9d\95\8a[T1].
+lemma lift_simple_sn: â\88\80d,e,T1,T2. â\87§[d, e] T1 â\89¡ T2 â\86\92 ð\9d\90\92[T2] â\86\92 ð\9d\90\92[T1].
#d #e #T1 #T2 #H elim H -d -e -T1 -T2 //
#I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #H
elim (simple_inv_bind … H)
(* Basic forward lemmas *****************************************************)
-lemma lifts_simple_dx: â\88\80T1,T2,des. â\87§*[des] T1 â\89¡ T2 â\86\92 ð\9d\95\8a[T1] â\86\92 ð\9d\95\8a[T2].
+lemma lifts_simple_dx: â\88\80T1,T2,des. â\87§*[des] T1 â\89¡ T2 â\86\92 ð\9d\90\92[T1] â\86\92 ð\9d\90\92[T2].
#T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_dx/
qed-.
-lemma lifts_simple_sn: â\88\80T1,T2,des. â\87§*[des] T1 â\89¡ T2 â\86\92 ð\9d\95\8a[T2] â\86\92 ð\9d\95\8a[T1].
+lemma lifts_simple_sn: â\88\80T1,T2,des. â\87§*[des] T1 â\89¡ T2 â\86\92 ð\9d\90\92[T2] â\86\92 ð\9d\90\92[T1].
#T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_sn/
qed-.
%.stats: CHARS = $(shell cat $(MAS) | wc -c)
+%.stats: C1 = $(shell grep "inductive\|record" $(MAS) | wc -l)
+%.stats: C2 = $(shell grep "definition\|let rec" $(MAS) | wc -l)
+%.stats: P1 = $(shell grep "theorem " $(MAS) | wc -l)
+%.stats: P2 = $(shell grep "lemma " $(MAS) | wc -l)
+
+%.stats: TBL = ld_$*_sum
+
%.stats:
@printf '\x1B[1;40;37m'
@printf '%-15s %-42s' 'Statistics for:' $*
# @printf ' %-6s %3i' Files `ls *.v | wc -l`
@printf '\x1B[0m\n'
@printf '\x1B[1;40;32m'
- @printf '%-8s %6i' Theorems `grep theorem $(MAS) | wc -l`
- @printf ' %-8s %5i' Lemmas `grep lemma $(MAS) | wc -l`
- @printf ' %-6s %3i' Facts `grep fact $(MAS) | wc -l`
+ @printf '%-8s %6i' Theorems `grep "theorem " $(MAS) | wc -l`
+ @printf ' %-8s %5i' Lemmas `grep "lemma " $(MAS) | wc -l`
+ @printf ' %-6s %3i' Facts `grep "fact " $(MAS) | wc -l`
@printf ' %-6s %3i' Proofs `grep qed $(MAS) | wc -l`
@printf '\x1B[0m\n'
@printf '\x1B[1;40;33m'
@printf ' %-6s %3i' Marks `grep "(\*\*)" $(MAS) | wc -l`
@printf ' %-10s' ''
@printf '\x1B[0m\n'
+ @printf 'name "$(TBL)"\n\n' > $*/$(TBL).tbl
+ @printf 'table {\n' >> $*/$(TBL).tbl
+ @printf ' class "grey" [ "category"\n' >> $*/$(TBL).tbl
+ @printf ' [ "objects" * ]\n' >> $*/$(TBL).tbl
+ @printf ' ]\n' >> $*/$(TBL).tbl
+ @printf ' class "green" [ "propositions"\n' >> $*/$(TBL).tbl
+ @printf ' [ "theorems" "$(P1)" * ]\n' >> $*/$(TBL).tbl
+ @printf ' [ "lemmas" "$(P2)" * ]\n' >> $*/$(TBL).tbl
+ @printf ' ]\n' >> $*/$(TBL).tbl
+ @printf ' class "yellow" [ "concepts"\n' >> $*/$(TBL).tbl
+ @printf ' [ "declared" "$(C1)" * ]\n' >> $*/$(TBL).tbl
+ @printf ' [ "defined" "$(C2)" * ]\n' >> $*/$(TBL).tbl
+ @printf ' ]\n' >> $*/$(TBL).tbl
+ @printf '}\n\n' >> $*/$(TBL).tbl
+ @printf 'class "component" { 0 }\n\n' >> $*/$(TBL).tbl
+ @printf 'class "plane" { 1 } { 3 } \n\n' >> $*/$(TBL).tbl
+ @printf 'class "number" { 2 } { 4 } \n\n' >> $*/$(TBL).tbl
projects / helm.git / commitdiff