diff options
Diffstat (limited to 'theories/Structures/OrdersTac.v')
| -rw-r--r-- | theories/Structures/OrdersTac.v | 293 |
1 files changed, 293 insertions, 0 deletions
diff --git a/theories/Structures/OrdersTac.v b/theories/Structures/OrdersTac.v new file mode 100644 index 00000000..66a672c9 --- /dev/null +++ b/theories/Structures/OrdersTac.v @@ -0,0 +1,293 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +Require Import Setoid Morphisms Basics Equalities Orders. +Set Implicit Arguments. + +(** * The order tactic *) + +(** This tactic is designed to solve systems of (in)equations + involving [eq], [lt], [le] and [~eq] on some type. This tactic is + domain-agnostic; it will only use equivalence+order axioms, and + not analyze elements of the domain. Hypothesis or goal of the form + [~lt] or [~le] are initially turned into [le] and [lt], other + parts of the goal are ignored. This initial preparation of the + goal is the only moment where totality is used. In particular, + the core of the tactic only proceeds by saturation of transitivity + and similar properties, and does not perform case splitting. + The tactic will fail if it doesn't solve the goal. *) + + +(** An abstract vision of the predicates. This allows a one-line + statement for interesting transitivity properties: for instance + [trans_ord OLE OLE = OLE] will imply later + [le x y -> le y z -> le x z]. +*) + +Inductive ord := OEQ | OLT | OLE. +Definition trans_ord o o' := + match o, o' with + | OEQ, _ => o' + | _, OEQ => o + | OLE, OLE => OLE + | _, _ => OLT + end. +Local Infix "+" := trans_ord. + + +(** ** The requirements of the tactic : [TotalOrder]. + + [TotalOrder] contains an equivalence [eq], + a strict order [lt] total and compatible with [eq], and + a larger order [le] synonym for [lt\/eq]. +*) + +(** ** Properties that will be used by the [order] tactic *) + +Module OrderFacts(Import O:TotalOrder'). + +(** Reflexivity rules *) + +Lemma eq_refl : forall x, x==x. +Proof. reflexivity. Qed. + +Lemma le_refl : forall x, x<=x. +Proof. intros; rewrite le_lteq; right; reflexivity. Qed. + +Lemma lt_irrefl : forall x, ~ x<x. +Proof. intros; apply StrictOrder_Irreflexive. Qed. + +(** Symmetry rules *) + +Lemma eq_sym : forall x y, x==y -> y==x. +Proof. auto with *. Qed. + +Lemma le_antisym : forall x y, x<=y -> y<=x -> x==y. +Proof. + intros x y; rewrite 2 le_lteq. intuition. + elim (StrictOrder_Irreflexive x); transitivity y; auto. +Qed. + +Lemma neq_sym : forall x y, ~x==y -> ~y==x. +Proof. auto using eq_sym. Qed. + +(** Transitivity rules : first, a generic formulation, then instances*) + +Ltac subst_eqns := + match goal with + | H : _==_ |- _ => (rewrite H || rewrite <- H); clear H; subst_eqns + | _ => idtac + end. + +Definition interp_ord o := + match o with OEQ => O.eq | OLT => O.lt | OLE => O.le end. +Local Notation "#" := interp_ord. + +Lemma trans : forall o o' x y z, #o x y -> #o' y z -> #(o+o') x z. +Proof. +destruct o, o'; simpl; intros x y z; rewrite ?le_lteq; intuition; + subst_eqns; eauto using (StrictOrder_Transitive x y z) with *. +Qed. + +Definition eq_trans x y z : x==y -> y==z -> x==z := @trans OEQ OEQ x y z. +Definition le_trans x y z : x<=y -> y<=z -> x<=z := @trans OLE OLE x y z. +Definition lt_trans x y z : x<y -> y<z -> x<z := @trans OLT OLT x y z. +Definition le_lt_trans x y z : x<=y -> y<z -> x<z := @trans OLE OLT x y z. +Definition lt_le_trans x y z : x<y -> y<=z -> x<z := @trans OLT OLE x y z. +Definition eq_lt x y z : x==y -> y<z -> x<z := @trans OEQ OLT x y z. +Definition lt_eq x y z : x<y -> y==z -> x<z := @trans OLT OEQ x y z. +Definition eq_le x y z : x==y -> y<=z -> x<=z := @trans OEQ OLE x y z. +Definition le_eq x y z : x<=y -> y==z -> x<=z := @trans OLE OEQ x y z. + +Lemma eq_neq : forall x y z, x==y -> ~y==z -> ~x==z. +Proof. eauto using eq_trans, eq_sym. Qed. + +Lemma neq_eq : forall x y z, ~x==y -> y==z -> ~x==z. +Proof. eauto using eq_trans, eq_sym. Qed. + +(** (double) negation rules *) + +Lemma not_neq_eq : forall x y, ~~x==y -> x==y. +Proof. +intros x y H. destruct (lt_total x y) as [H'|[H'|H']]; auto; + destruct H; intro H; rewrite H in H'; eapply lt_irrefl; eauto. +Qed. + +Lemma not_ge_lt : forall x y, ~y<=x -> x<y. +Proof. +intros x y H. destruct (lt_total x y); auto. +destruct H. rewrite le_lteq. intuition. +Qed. + +Lemma not_gt_le : forall x y, ~y<x -> x<=y. +Proof. +intros x y H. rewrite le_lteq. generalize (lt_total x y); intuition. +Qed. + +Lemma le_neq_lt : forall x y, x<=y -> ~x==y -> x<y. +Proof. auto using not_ge_lt, le_antisym. Qed. + +End OrderFacts. + + + +(** ** [MakeOrderTac] : The functor providing the order tactic. *) + +Module MakeOrderTac (Import O:TotalOrder'). + +Include OrderFacts O. + +(** order_eq : replace x by y in all (in)equations hyps thanks + to equality EQ (where eq has been hidden in order to avoid + self-rewriting), then discard EQ. *) + +Ltac order_rewr x eqn := + (* NB: we could use the real rewrite here, but proofs would be uglier. *) + let rewr H t := generalize t; clear H; intro H + in + match goal with + | H : x == _ |- _ => rewr H (eq_trans (eq_sym eqn) H); order_rewr x eqn + | H : _ == x |- _ => rewr H (eq_trans H eqn); order_rewr x eqn + | H : ~x == _ |- _ => rewr H (eq_neq (eq_sym eqn) H); order_rewr x eqn + | H : ~_ == x |- _ => rewr H (neq_eq H eqn); order_rewr x eqn + | H : x < _ |- _ => rewr H (eq_lt (eq_sym eqn) H); order_rewr x eqn + | H : _ < x |- _ => rewr H (lt_eq H eqn); order_rewr x eqn + | H : x <= _ |- _ => rewr H (eq_le (eq_sym eqn) H); order_rewr x eqn + | H : _ <= x |- _ => rewr H (le_eq H eqn); order_rewr x eqn + | _ => clear eqn +end. + +Ltac order_eq x y eqn := + match x with + | y => clear eqn + | _ => change (interp_ord OEQ x y) in eqn; order_rewr x eqn + end. + +(** Goal preparation : We turn all negative hyps into positive ones + and try to prove False from the inverse of the current goal. + These steps require totality of our order. After this preparation, + order only deals with the context, and tries to prove False. + Hypotheses of the form [A -> False] are also folded in [~A] + for convenience (i.e. cope with the mess left by intuition). *) + +Ltac order_prepare := + match goal with + | H : ?A -> False |- _ => change (~A) in H; order_prepare + | H : ~(?R ?x ?y) |- _ => + match R with + | eq => fail 1 (* if already using [eq], we leave it this ways *) + | _ => (change (~x==y) in H || + apply not_gt_le in H || + apply not_ge_lt in H || + clear H || fail 1); order_prepare + end + | H : ?R ?x ?y |- _ => + match R with + | eq => fail 1 + | lt => fail 1 + | le => fail 1 + | _ => (change (x==y) in H || + change (x<y) in H || + change (x<=y) in H || + clear H || fail 1); order_prepare + end + | |- ~ _ => intro; order_prepare + | |- _ ?x ?x => + exact (eq_refl x) || exact (le_refl x) || exfalso + | _ => + (apply not_neq_eq; intro) || + (apply not_ge_lt; intro) || + (apply not_gt_le; intro) || exfalso + end. + +(** We now try to prove False from the various [< <= == !=] hypothesis *) + +Ltac order_loop := + match goal with + (* First, successful situations *) + | H : ?x < ?x |- _ => exact (lt_irrefl H) + | H : ~ ?x == ?x |- _ => exact (H (eq_refl x)) + (* Second, useless hyps *) + | H : ?x <= ?x |- _ => clear H; order_loop + (* Third, we eliminate equalities *) + | H : ?x == ?y |- _ => order_eq x y H; order_loop + (* Simultaneous le and ge is eq *) + | H1 : ?x <= ?y, H2 : ?y <= ?x |- _ => + generalize (le_antisym H1 H2); clear H1 H2; intro; order_loop + (* Simultaneous le and ~eq is lt *) + | H1: ?x <= ?y, H2: ~ ?x == ?y |- _ => + generalize (le_neq_lt H1 H2); clear H1 H2; intro; order_loop + | H1: ?x <= ?y, H2: ~ ?y == ?x |- _ => + generalize (le_neq_lt H1 (neq_sym H2)); clear H1 H2; intro; order_loop + (* Transitivity of lt and le *) + | H1 : ?x < ?y, H2 : ?y < ?z |- _ => + match goal with + | H : x < z |- _ => fail 1 + | _ => generalize (lt_trans H1 H2); intro; order_loop + end + | H1 : ?x <= ?y, H2 : ?y < ?z |- _ => + match goal with + | H : x < z |- _ => fail 1 + | _ => generalize (le_lt_trans H1 H2); intro; order_loop + end + | H1 : ?x < ?y, H2 : ?y <= ?z |- _ => + match goal with + | H : x < z |- _ => fail 1 + | _ => generalize (lt_le_trans H1 H2); intro; order_loop + end + | H1 : ?x <= ?y, H2 : ?y <= ?z |- _ => + match goal with + | H : x <= z |- _ => fail 1 + | _ => generalize (le_trans H1 H2); intro; order_loop + end + | _ => idtac +end. + +(** The complete tactic. *) + +Ltac order := + intros; order_prepare; order_loop; fail "Order tactic unsuccessful". + +End MakeOrderTac. + +Module OTF_to_OrderTac (OTF:OrderedTypeFull). + Module TO := OTF_to_TotalOrder OTF. + Include !MakeOrderTac TO. +End OTF_to_OrderTac. + +Module OT_to_OrderTac (OT:OrderedType). + Module OTF := OT_to_Full OT. + Include !OTF_to_OrderTac OTF. +End OT_to_OrderTac. + +Module TotalOrderRev (O:TotalOrder) <: TotalOrder. + +Definition t := O.t. +Definition eq := O.eq. +Definition lt := flip O.lt. +Definition le := flip O.le. +Include EqLtLeNotation. + +(* No Instance syntax to avoid saturating the Equivalence tables *) +Definition eq_equiv := O.eq_equiv. + +Instance lt_strorder: StrictOrder lt. +Proof. unfold lt; auto with *. Qed. +Instance lt_compat : Proper (eq==>eq==>iff) lt. +Proof. unfold lt; auto with *. Qed. + +Lemma le_lteq : forall x y, x<=y <-> x<y \/ x==y. +Proof. intros; unfold le, lt, flip. rewrite O.le_lteq; intuition. Qed. + +Lemma lt_total : forall x y, x<y \/ x==y \/ y<x. +Proof. + intros x y; unfold lt, eq, flip. + generalize (O.lt_total x y); intuition. +Qed. + +End TotalOrderRev. |