Library ATBR.Graph
Basic properties, definitions and hints about the Classes.Graph base-class
projections, for auto, or to help in manual proofs
Lemma equal_refl x: equal A B x x.
Lemma equal_sym x y: equal A B x y -> equal A B y x.
Lemma equal_trans x y z: equal A B x y -> equal A B y z -> equal A B x z.
Lemma equal_sym x y: equal A B x y -> equal A B y x.
Lemma equal_trans x y z: equal A B x y -> equal A B y z -> equal A B x z.
Lemmas to solve automatically some index related goals (a la f_equal)
Lemma equal_refl_f1 (f: nat -> X A B):
forall i i', i = i' -> f i == f i'.
Lemma equal_refl_f2 (f: nat -> nat -> X A B):
forall i i' j j', i=i' -> j=j' -> f i j == f i' j'.
Lemma equal_refl_f1t Z (f: nat -> Z -> X A B):
forall t i i', i = i' -> f i t == f i' t.
Lemma equal_refl_f2t Z (f: nat -> nat -> Z -> X A B):
forall t i i' j j', i=i' -> j=j' -> f i j t == f i' j' t.
forall i i', i = i' -> f i == f i'.
Lemma equal_refl_f2 (f: nat -> nat -> X A B):
forall i i' j j', i=i' -> j=j' -> f i j == f i' j'.
Lemma equal_refl_f1t Z (f: nat -> Z -> X A B):
forall t i i', i = i' -> f i t == f i' t.
Lemma equal_refl_f2t Z (f: nat -> nat -> Z -> X A B):
forall t i i' j j', i=i' -> j=j' -> f i j t == f i' j' t.
boolean test
Definition xif (b: bool) (x y: X A B) := if b then x else y.
Global Instance xif_compat: Proper (@eq bool ==> equal A B ==> equal A B ==> equal A B) xif.
Lemma xif_spec: forall b x y z, (b=true -> x==z) -> (b=false -> y==z) -> xif b x y == z.
Lemma xif_false: forall b x y, b=false -> xif b x y == y.
Lemma xif_true: forall b x y, b=true -> xif b x y == x.
Lemma xif_idem: forall b x, xif b x x == x.
Lemma xif_idem': forall b x y, x == y -> xif b x y == x.
Lemma xif_xif_and: forall b c x y, xif b (xif c x y) y == xif (b&&c) x y.
Lemma xif_xif_or: forall b c x y, xif b x (xif c x y) == xif (b||c) x y.
Lemma xif_negb: forall b x y, xif (negb b) x y == xif b y x.
End equal.
Lemma fun_xif {G G': Graph} A B A' B' (f: @X G A B -> @X G' A' B') b x y: f (xif b x y) == xif b (f x) (f y).
Section leq.
Global Instance xif_compat: Proper (@eq bool ==> equal A B ==> equal A B ==> equal A B) xif.
Lemma xif_spec: forall b x y z, (b=true -> x==z) -> (b=false -> y==z) -> xif b x y == z.
Lemma xif_false: forall b x y, b=false -> xif b x y == y.
Lemma xif_true: forall b x y, b=true -> xif b x y == x.
Lemma xif_idem: forall b x, xif b x x == x.
Lemma xif_idem': forall b x y, x == y -> xif b x y == x.
Lemma xif_xif_and: forall b c x y, xif b (xif c x y) y == xif (b&&c) x y.
Lemma xif_xif_or: forall b c x y, xif b x (xif c x y) == xif (b||c) x y.
Lemma xif_negb: forall b x y, xif (negb b) x y == xif b y x.
End equal.
Lemma fun_xif {G G': Graph} A B A' B' (f: @X G A B -> @X G' A' B') b x y: f (xif b x y) == xif b (f x) (f y).
Section leq.
Basic properties of the underlying preorder
Context `{SL: SemiLattice}.
Variables A B: T.
Global Instance leq_refl: Reflexive (leq A B).
Global Instance leq_trans: Transitive (leq A B).
Global Instance equal_leq: subrelation (equal A B) (leq A B).
Global Instance equal_geq: subrelation (equal A B) (inverse (leq A B)).
Definition leq_antisym: Antisymmetric _ _ (leq A B).
Qed.
End leq.
Hint Resolve @equal_refl.
Hint Immediate @equal_sym.
Hint Resolve @equal_refl_f1 @equal_refl_f2.
Hint Extern 1 (equal ?A ?B (?f (_: nat) ?t) (?f _ ?t)) => apply @equal_refl_f1t.
Hint Extern 2 (equal ?A ?B (?f (_: nat) (_: nat) ?t) (?f _ _ ?t)) => apply @equal_refl_f2t.
Hint Extern 3 (_ == _) => apply @xif_compat.
Variables A B: T.
Global Instance leq_refl: Reflexive (leq A B).
Global Instance leq_trans: Transitive (leq A B).
Global Instance equal_leq: subrelation (equal A B) (leq A B).
Global Instance equal_geq: subrelation (equal A B) (inverse (leq A B)).
Definition leq_antisym: Antisymmetric _ _ (leq A B).
Qed.
End leq.
Hint Resolve @equal_refl.
Hint Immediate @equal_sym.
Hint Resolve @equal_refl_f1 @equal_refl_f2.
Hint Extern 1 (equal ?A ?B (?f (_: nat) ?t) (?f _ ?t)) => apply @equal_refl_f1t.
Hint Extern 2 (equal ?A ?B (?f (_: nat) (_: nat) ?t) (?f _ _ ?t)) => apply @equal_refl_f2t.
Hint Extern 3 (_ == _) => apply @xif_compat.