Library fl.aut.glue
(*
Authors: Thierry Coquand, Vincent Siles
*)
Authors: Thierry Coquand, Vincent Siles
*)
Definition of the eqType structure of the 3 states type _comparison_
Lemma comparison_negK : ∀ s t, s = CompOpp t → t = CompOpp s.
Fixpoint eq_comparison (a b:comparison) : bool := match a,b with
| Lt,Lt ⇒ true
| Eq,Eq ⇒ true
| Gt,Gt ⇒ true
| _,_ ⇒ false
end.
Lemma eq_comparison_axiom : Equality.axiom eq_comparison.
Definition comparison_eq_mixin := EqMixin eq_comparison_axiom.
Canonical Structure comparison_eqType := EqType comparison
comparison_eq_mixin.
Fixpoint eq_comparison (a b:comparison) : bool := match a,b with
| Lt,Lt ⇒ true
| Eq,Eq ⇒ true
| Gt,Gt ⇒ true
| _,_ ⇒ false
end.
Lemma eq_comparison_axiom : Equality.axiom eq_comparison.
Definition comparison_eq_mixin := EqMixin eq_comparison_axiom.
Canonical Structure comparison_eqType := EqType comparison
comparison_eq_mixin.
Definition of a canonical structure of an eqType with a 3 states
total comparison function
Record osym_module_mixin (symbol:eqType) : Type := OSymModuleMixin{
cmp : symbol → symbol → comparison;
cmp_refl : ∀ s, cmp s s = Eq;
cmp_eq_axiom : ∀ s t, reflect (s = t) (cmp s t == Eq);
cmp_trans : ∀ (s t u:symbol) (x:comparison),
cmp s t = x → cmp t u = x → cmp s u = x;
cmp_neg : ∀ (s t:symbol), cmp t s = CompOpp (cmp s t)
}.
Record osym_module : Type := OSymModule {
carrier :> eqType;
spec : osym_module_mixin carrier
}.
Definition cmpS (s:osym_module) := cmp (spec s).
Definition leS (S:osym_module) := fun (x y:S) ⇒ if cmpS x y is Gt then false else true.
Lemma cmpS_refl : ∀ (S:osym_module) (b:S), cmpS b b = Eq.
Lemma cmpS_eq_axiom : ∀ (S:osym_module) (a b:S), reflect (a = b) (cmpS a b == Eq).
Lemma cmpS_trans : ∀ (S:osym_module) (a b c:S) (x: comparison),
cmpS a b = x → cmpS b c = x → cmpS a c = x.
Lemma cmpS_neg : ∀ (S:osym_module) (a b: S),
cmpS a b = CompOpp (cmpS b a).
Lemma leS_refl : ∀ (S:osym_module), reflexive (@leS S).
Lemma leS_trans : ∀ (S:osym_module), transitive (@leS S).
Lemma leS_antisym : ∀ (S: osym_module), antisymmetric (@leS S).
Lemma leS_total : ∀ (S:osym_module), total (@leS S).
cmp : symbol → symbol → comparison;
cmp_refl : ∀ s, cmp s s = Eq;
cmp_eq_axiom : ∀ s t, reflect (s = t) (cmp s t == Eq);
cmp_trans : ∀ (s t u:symbol) (x:comparison),
cmp s t = x → cmp t u = x → cmp s u = x;
cmp_neg : ∀ (s t:symbol), cmp t s = CompOpp (cmp s t)
}.
Record osym_module : Type := OSymModule {
carrier :> eqType;
spec : osym_module_mixin carrier
}.
Definition cmpS (s:osym_module) := cmp (spec s).
Definition leS (S:osym_module) := fun (x y:S) ⇒ if cmpS x y is Gt then false else true.
Lemma cmpS_refl : ∀ (S:osym_module) (b:S), cmpS b b = Eq.
Lemma cmpS_eq_axiom : ∀ (S:osym_module) (a b:S), reflect (a = b) (cmpS a b == Eq).
Lemma cmpS_trans : ∀ (S:osym_module) (a b c:S) (x: comparison),
cmpS a b = x → cmpS b c = x → cmpS a c = x.
Lemma cmpS_neg : ∀ (S:osym_module) (a b: S),
cmpS a b = CompOpp (cmpS b a).
Lemma leS_refl : ∀ (S:osym_module), reflexive (@leS S).
Lemma leS_trans : ∀ (S:osym_module), transitive (@leS S).
Lemma leS_antisym : ∀ (S: osym_module), antisymmetric (@leS S).
Lemma leS_total : ∀ (S:osym_module), total (@leS S).
Some very general definitions and missing
properties in ssreflect stdlib
Section Glue.
Variable A B: Type.
Fixpoint seq_to_list (s:seq A) : list A := match s with
| nil ⇒ List.nil
| hd:: tl ⇒ (hd::(seq_to_list tl))%list
end.
Lemma flatten_cat: ∀ (l l':seq (seq A)) ,
flatten (l++l') = flatten l ++ flatten l'.
Lemma flatten_map_cons : ∀ (l:seq A),
flatten (map (fun xx ⇒ [::xx]) l) = l.
Definition dupl (X: seq (A×B)) : seq (A×A×B) :=
map (fun (ab:A×B) ⇒ let (a,b) := ab in (a,a,b)) X.
Definition strip (X: seq (A×A×B)) : seq (A×B) :=
map (fun ab:A×A×B ⇒ let (aa,b) := ab in let (a,_) := aa in (a,b)) X.
Lemma dupl_strip : ∀ (X:seq (A×B)), strip (dupl X) = X.
End Glue.
Section Glue2.
Variable T T':eqType.
Variable R: rel T.
Variable A B: Type.
Fixpoint seq_to_list (s:seq A) : list A := match s with
| nil ⇒ List.nil
| hd:: tl ⇒ (hd::(seq_to_list tl))%list
end.
Lemma flatten_cat: ∀ (l l':seq (seq A)) ,
flatten (l++l') = flatten l ++ flatten l'.
Lemma flatten_map_cons : ∀ (l:seq A),
flatten (map (fun xx ⇒ [::xx]) l) = l.
Definition dupl (X: seq (A×B)) : seq (A×A×B) :=
map (fun (ab:A×B) ⇒ let (a,b) := ab in (a,a,b)) X.
Definition strip (X: seq (A×A×B)) : seq (A×B) :=
map (fun ab:A×A×B ⇒ let (aa,b) := ab in let (a,_) := aa in (a,b)) X.
Lemma dupl_strip : ∀ (X:seq (A×B)), strip (dupl X) = X.
End Glue.
Section Glue2.
Variable T T':eqType.
Variable R: rel T.
some usefull lemmas to deal with sorted + undup sequences
Lemma path_undup : ∀ (hR : transitive R) l (x:T), path R x l → path R x (undup l).
Lemma sorted_undup : ∀ (hR: transitive R) (l:seq T), sorted R l → sorted R (undup l).
Lemma tool_undup_size : ∀ (l l': seq T), size (undup l') ≤ size (undup (l++l')).
Lemma tool_undup_size2 : ∀ (l l': seq T), size (undup l) ≤ size (undup (l++l')).
Lemma merge_sort_sym : ∀ (hR1:transitive R) (hR2: antisymmetric R) (hR3: total R)
(l1 l2:seq T), sorted R l1 → sorted R l2 → merge R l1 l2 = merge R l2 l1.
Lemma tool_normP_in : ∀ (hd:T) tl l, perm_eq (hd::tl) l →
∃ l1, ∃ l2, l = l1 ++ hd :: l2 ∧ tl =i l1 ++ l2.
Lemma sorted_undup : ∀ (hR: transitive R) (l:seq T), sorted R l → sorted R (undup l).
Lemma tool_undup_size : ∀ (l l': seq T), size (undup l') ≤ size (undup (l++l')).
Lemma tool_undup_size2 : ∀ (l l': seq T), size (undup l) ≤ size (undup (l++l')).
Lemma merge_sort_sym : ∀ (hR1:transitive R) (hR2: antisymmetric R) (hR3: total R)
(l1 l2:seq T), sorted R l1 → sorted R l2 → merge R l1 l2 = merge R l2 l1.
Lemma tool_normP_in : ∀ (hd:T) tl l, perm_eq (hd::tl) l →
∃ l1, ∃ l2, l = l1 ++ hd :: l2 ∧ tl =i l1 ++ l2.
boolean operator to check inclusion of lists:
lincl l l' means that forall x in l, x is in l'
Fixpoint lincl (l l':seq T) : bool :=
match l with
| [::] ⇒ true
| hd :: tl ⇒ (hd \in l') && (lincl tl l')
end.
Lemma lincl_cons : ∀ (l l1:seq T) a, lincl l l1 → lincl l (a::l1).
Lemma lincl_catr : ∀ (l l1 l2: seq T), lincl l l1 → lincl l (l1 ++ l2).
Lemma lincl_refl : ∀ (l:seq T), lincl l l.
Lemma lincl_nil : ∀ (l:seq T), lincl l [::] → l = [::].
Lemma linclP : ∀ (l l':seq T),
reflect (∀ a, (a \in l) → (a \in l')) (lincl l l').
Lemma lincl_mem: ∀ (l l': seq T), lincl l l' →
∀ a, (a\in l) → (a \in l').
Lemma lincl_trans : transitive lincl.
Lemma strip_in : ∀ (X: seq (T×T×T')) (a a':T) (b:T'),
(a,a',b) \in X → (a,b) \in (strip X).
End Glue2.
match l with
| [::] ⇒ true
| hd :: tl ⇒ (hd \in l') && (lincl tl l')
end.
Lemma lincl_cons : ∀ (l l1:seq T) a, lincl l l1 → lincl l (a::l1).
Lemma lincl_catr : ∀ (l l1 l2: seq T), lincl l l1 → lincl l (l1 ++ l2).
Lemma lincl_refl : ∀ (l:seq T), lincl l l.
Lemma lincl_nil : ∀ (l:seq T), lincl l [::] → l = [::].
Lemma linclP : ∀ (l l':seq T),
reflect (∀ a, (a \in l) → (a \in l')) (lincl l l').
Lemma lincl_mem: ∀ (l l': seq T), lincl l l' →
∀ a, (a\in l) → (a \in l').
Lemma lincl_trans : transitive lincl.
Lemma strip_in : ∀ (X: seq (T×T×T')) (a a':T) (b:T'),
(a,a',b) \in X → (a,b) \in (strip X).
End Glue2.