--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "hvbox( ∁ term 70 t )"
+ non associative with precedence 70
+ for @{ 'Complement $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 *)
-(* *)
-(**************************************************************************)
-
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
-
-notation "hvbox( 𝐈 ⦃ term 46 f ⦄ )"
- non associative with precedence 45
- for @{ 'IsId $f }.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "hvbox( 𝐈 ⦃ term 46 f ⦄ )"
+ non associative with precedence 45
+ for @{ 'IsIdentity $f }.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "hvbox( 𝐔 ⦃ term 46 f ⦄ )"
+ non associative with precedence 45
+ for @{ 'IsUniform $f }.
#cs #i1 #i2 #_ * /3 width=1 by le_S_S, conj/
qed-.
-lemma at_inv_gt1: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → ∥cs∥ < i1 → ⊥.
+lemma at_inv_gt1: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → ∥cs∥ < i1 → ⊥.
#cs #i1 #i2 #H elim (at_inv_le … H) -H /2 width=4 by lt_le_false/
qed-.
(* *)
(**************************************************************************)
-include "ground_2/notation/relations/isid_1.ma".
+include "ground_2/notation/relations/isidentity_1.ma".
include "ground_2/relocation/trace_after.ma".
+include "ground_2/relocation/trace_sle.ma".
(* RELOCATION TRACE *********************************************************)
definition isid: predicate trace ≝ λcs. ∥cs∥ = |cs|.
interpretation "test for identity (trace)"
- 'IsId cs = (isid cs).
+ 'IsIdentity cs = (isid cs).
+
+definition t_reflexive: ∀S:Type[0]. predicate (trace → relation S) ≝
+ λS,R. ∀a. ∃∃t. 𝐈⦃t⦄ & R t a a.
(* Basic properties *********************************************************)
| #t1 #t2 #t #_ #_ #H elim (isid_inv_false … H)
]
qed-.
+
+(* Forward on inclusion *****************************************************)
+
+lemma sle_isid1_fwd: ∀t1,t2. t1 ⊆ t2 → 𝐈⦃t1⦄ → t1 = t2.
+#t1 #t2 #H elim H -t1 -t2 //
+[ #t1 #t2 #_ #IH #H lapply (isid_inv_true … H) -H
+ #HT1 @eq_f2 // @IH @HT1 (**) (* full auto fails *)
+| #t1 #t2 #b #_ #_ #H elim (isid_inv_false … 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 "ground_2/notation/relations/isuniform_1.ma".
+include "ground_2/relocation/trace_isid.ma".
+
+(* RELOCATION TRACE *********************************************************)
+
+inductive isun: predicate trace ≝
+| isun_id : ∀t. 𝐈⦃t⦄ → isun t
+| isun_false: ∀t. isun t → isun (Ⓕ@t)
+.
+
+interpretation "test for uniformity (trace)"
+ 'IsUniform t = (isun t).
+
+(* Basic inversion lennas ***************************************************)
+
+fact isun_inv_true_aux: ∀t. 𝐔⦃t⦄ → ∀u. t = Ⓣ@u → 𝐈⦃u⦄.
+#t * -t
+[ #t #Ht #u #H destruct /2 width=1 by isid_inv_true/
+| #t #_ #u #H destruct
+]
+qed-.
+
+lemma isun_inv_true: ∀t. 𝐔⦃Ⓣ@t⦄ → 𝐈⦃t⦄.
+/2 width=3 by isun_inv_true_aux/ qed-.
+
+fact isun_inv_false_aux: ∀t. 𝐔⦃t⦄ → ∀u. t = Ⓕ@u → 𝐔⦃u⦄.
+#t * -t
+[ #t #Ht #u #H destruct elim (isid_inv_false … Ht)
+| #t #Ht #u #H destruct //
+]
+qed-.
+
+lemma isun_inv_false: ∀t. 𝐔⦃Ⓕ@t⦄ → 𝐔⦃t⦄.
+/2 width=3 by isun_inv_false_aux/ 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 "ground_2/relocation/trace_at.ma".
+
+(* RELOCATION TRACE *********************************************************)
+
+inductive sle: relation trace ≝
+| sle_empty: sle (◊) (◊)
+| sle_true : ∀t1,t2. sle t1 t2 → sle (Ⓣ @ t1) (Ⓣ @ t2)
+| sle_false: ∀t1,t2,b. sle t1 t2 → sle (Ⓕ @ t1) (b @ t2)
+.
+
+interpretation
+ "inclusion (trace)"
+ 'subseteq t1 t2 = (sle t1 t2).
+
+(* Basic properties *********************************************************)
+
+(* Basic forward lemmas *****************************************************)
+
+lemma sle_fwd_length: ∀t1,t2. t1 ⊆ t2 → |t1| = |t2|.
+#t1 #t2 #H elim H -t1 -t2 //
+qed-.
+
+lemma sle_fwd_colength: ∀t1,t2. t1 ⊆ t2 → ∥t1∥ ≤ ∥t2∥.
+#t1 #t2 #H elim H -t1 -t2 /2 width=1 by le_S_S/
+#t1 #t2 * /2 width=1 by le_S/
+qed-.
+
+(* Inversion lemmas on application ******************************************)
+
+lemma sle_inv_at: ∀t1,t2. t1 ⊆ t2 →
+ ∀i,i1,i2. @⦃i, t1⦄ ≡ i1 → @⦃i, t2⦄ ≡ i2 → i2 ≤ i1.
+#t1 #t2 #H elim H -t1 -t2
+[ #i #i1 #i2 #_ #H2 elim (at_inv_empty … H2) -H2 //
+| #t1 #t2 #_ #IH #i #i1 #i2 #H0 #H2 elim (at_inv_true … H2) -H2 * //
+ #j1 #j2 #H1 #H2 #Hj destruct elim (at_inv_true_succ_sn … H0) -H0
+ /3 width=3 by le_S_S/
+| #t1 #t2 * #_ #IH #i #i1 #i2 #H0 #H2
+ [ elim (at_inv_true … H2) -H2 * //
+ #j #j2 #H1 #H2 #Hj2 destruct elim (at_inv_false … H0) -H0
+ #j1 #H #Hj1 destruct elim (at_monotonic … Hj1 j) -Hj1 //
+ #x #H1x #H2x @le_S_S /4 width=3 by lt_to_le, le_to_lt_to_lt/ (**) (* full auto too slow *)
+ | elim (at_inv_false … H2) elim (at_inv_false … H0) -H0 -H2
+ /3 width=3 by le_S_S/
+ ]
+]
+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 "ground_2/notation/functions/complement_1.ma".
+include "ground_2/relocation/trace.ma".
+
+(* RELOCATION TRACE *********************************************************)
+
+let rec snot (t:trace) on t ≝ match t with
+[ nil ⇒ ◊
+| cons b t ⇒ (¬ b) @ snot t
+].
+
+interpretation
+ "complement (trace)"
+ 'Complement t = (snot t).
+
+(* Basic properties *********************************************************)
+
+lemma snot_empty: ∁ (◊) = ◊.
+// qed.
+
+lemma snot_inh: ∀t,b. ∁ (b@t) = (¬ b) @ ∁ t.
+// qed.
+
+lemma snot_true: ∀t. ∁ (Ⓣ @ t) = Ⓕ @ ∁ t.
+// qed.
+
+lemma snot_false: ∀t. ∁ (Ⓕ @ t) = Ⓣ @ ∁ t.
+// qed.
+
+lemma snot_length: ∀t. |∁ t| = |t|.
+#t elim t -t normalize //
+qed.
+
+lemma snot_colength: ∀t. ∥∁ t∥ = |t| - ∥t∥.
+#t elim t -t //
+* /2 width=1 by minus_Sn_m/
+qed.
class "green"
[ { "multiple relocation" * } {
[ { "" * } {
- [ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_sor ( ? ⋓ ? ≡ ? )" * ]
+ [ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )"
+ "trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≡ ? )" "trace_snot ( ∁ ? )" * ]
[ "mr2" "mr2_at ( @⦃?,?⦄ ≡ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≡ ? )" * ]
}
]
try List.assoc "depth" a
with Not_found -> ""
in
- let trace = "/"^(if int_of_string depth > 1 then depth else "")^" by " in
+ let width =
+ try List.assoc "width" a
+ with Not_found -> ""
+ in
+ let trace = "/"^(if int_of_string depth > 1 then depth ^ " width=" ^ width else "")^" by " in
let thms =
match !trace_ref with
| [] -> ""
;;
let predefined_classes = [
- ["&"; "⅋"; ];
- ["!"; "¡"; "⫯"; "⫰"; ];
+ ["&"; "⅋"; ];
+ ["|"; "∥"; ];
+ ["!"; "¡"; "⫯"; "⫰"; ];
["?"; "¿"; "⸮"; ];
[":"; "⁝"; ];
["."; "•"; "◦"; ];
projects / helm.git / commitdiff