adamc@2: (* Copyright (c) 2008, Adam Chlipala adamc@2: * adamc@2: * This work is licensed under a adamc@2: * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 adamc@2: * Unported License. adamc@2: * The license text is available at: adamc@2: * http://creativecommons.org/licenses/by-nc-nd/3.0/ adamc@2: *) adamc@2: adamc@85: Require Import Eqdep List. adamc@2: adamc@38: Require Omega. adamc@38: adamc@59: Set Implicit Arguments. adamc@59: adamc@2: adamc@66: Ltac inject H := injection H; clear H; intros; try subst. adamc@51: adamc@59: Ltac appHyps f := adamc@50: match goal with adamc@59: | [ H : _ |- _ ] => f H adamc@59: end. adamc@59: adamc@59: Ltac inList x ls := adamc@59: match ls with adamc@59: | x => idtac adamc@84: | (_, x) => idtac adamc@59: | (?LS, _) => inList x LS adamc@59: end. adamc@59: adamc@59: Ltac app f ls := adamc@59: match ls with adamc@59: | (?LS, ?X) => f X || app f LS || fail 1 adamc@59: | _ => f ls adamc@59: end. adamc@59: adamc@59: Ltac all f ls := adamc@59: match ls with adamc@59: | (?LS, ?X) => f X; all f LS adamc@59: | (_, _) => fail 1 adamc@59: | _ => f ls adamc@59: end. adamc@59: adamc@59: Ltac simplHyp invOne := adamc@99: let invert H F := adamc@99: inList F invOne; (inversion H; fail) adamc@99: || (inversion H; [idtac]; clear H; try subst) in adamc@59: match goal with adamc@59: | [ H : ex _ |- _ ] => destruct H adamc@59: adamc@204: | [ H : ?F ?X = ?F ?Y |- ?G ] => adamc@204: (assert (X = Y); [ assumption | fail 1 ]) adamc@204: || (injection H; adamc@204: match goal with adamc@204: | [ |- X = Y -> G ] => adamc@204: try clear H; intros; try subst adamc@204: end) adamc@204: | [ H : ?F ?X ?U = ?F ?Y ?V |- ?G ] => adamc@204: (assert (X = Y); [ assumption adamc@204: | assert (U = V); [ assumption | fail 1 ] ]) adamc@204: || (injection H; adamc@204: match goal with adamc@204: | [ |- U = V -> X = Y -> G ] => adamc@204: try clear H; intros; try subst adamc@204: end) adamc@59: adamc@99: | [ H : ?F _ |- _ ] => invert H F adamc@99: | [ H : ?F _ _ |- _ ] => invert H F adamc@99: | [ H : ?F _ _ _ |- _ ] => invert H F adamc@99: | [ H : ?F _ _ _ _ |- _ ] => invert H F adamc@99: | [ H : ?F _ _ _ _ _ |- _ ] => invert H F adamc@176: adamc@176: | [ H : existT _ ?T _ = existT _ ?T _ |- _ ] => generalize (inj_pair2 _ _ _ _ _ H); clear H adamc@176: | [ H : existT _ _ _ = existT _ _ _ |- _ ] => inversion H; clear H adamc@179: adamc@179: | [ H : Some _ = Some _ |- _ ] => injection H; clear H adamc@50: end. adamc@50: adamc@2: Ltac rewriteHyp := adamc@2: match goal with adamc@183: | [ H : _ |- _ ] => rewrite H; auto; [idtac] adamc@2: end. adamc@2: adamc@2: Ltac rewriterP := repeat (rewriteHyp; autorewrite with cpdt in *). adamc@2: adamc@2: Ltac rewriter := autorewrite with cpdt in *; rewriterP. adamc@2: adamc@2: Hint Rewrite app_ass : cpdt. adamc@2: adamc@59: Definition done (T : Type) (x : T) := True. adamc@2: adamc@59: Ltac inster e trace := adamc@59: match type of e with adamc@59: | forall x : _, _ => adamc@59: match goal with adamc@59: | [ H : _ |- _ ] => adamc@59: inster (e H) (trace, H) adamc@59: | _ => fail 2 adamc@59: end adamc@59: | _ => adamc@59: match trace with adamc@59: | (_, _) => adamc@59: match goal with adamc@59: | [ H : done (trace, _) |- _ ] => fail 1 adamc@59: | _ => adamc@59: let T := type of e in adamc@59: match type of T with adamc@59: | Prop => adamc@59: generalize e; intro; adamc@59: assert (done (trace, tt)); [constructor | idtac] adamc@59: | _ => adamc@59: all ltac:(fun X => adamc@59: match goal with adamc@59: | [ H : done (_, X) |- _ ] => fail 1 adamc@59: | _ => idtac adamc@59: end) trace; adamc@59: let i := fresh "i" in (pose (i := e); adamc@59: assert (done (trace, i)); [constructor | idtac]) adamc@59: end adamc@59: end adamc@59: end adamc@59: end. adamc@59: adamc@65: Ltac un_done := adamc@65: repeat match goal with adamc@65: | [ H : done _ |- _ ] => clear H adamc@65: end. adamc@65: adamc@88: Ltac crush' lemmas invOne := adamc@184: let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence in adamc@184: let rewriter := autorewrite with cpdt in *; adamc@184: repeat (match goal with adamc@184: | [ H : _ |- _ ] => (rewrite H; []) adamc@184: || (rewrite H; [ | solve [ crush' lemmas invOne ] ]) adamc@184: || (rewrite H; [ | solve [ crush' lemmas invOne ] | solve [ crush' lemmas invOne ] ]) adamc@184: end; autorewrite with cpdt in *) adamc@184: in (sintuition; rewriter; adamc@183: match lemmas with adamc@183: | false => idtac adamc@183: | _ => repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L)); adamc@183: repeat (simplHyp invOne; intuition)); un_done adamc@184: end; sintuition; rewriter; sintuition; try omega; try (elimtype False; omega)). adamc@59: adamc@88: Ltac crush := crush' false fail. adamc@85: adamc@213: Require Import Program.Equality. adamc@85: adamc@85: Ltac dep_destruct E := adamc@213: let x := fresh "x" in adamc@213: remember E as x; simpl in x; dependent destruction x; adamc@213: try match goal with adamc@213: | [ H : _ = E |- _ ] => rewrite <- H in *; clear H adamc@213: end. adamc@118: adamc@118: Ltac clear_all := adamc@118: repeat match goal with adamc@118: | [ H : _ |- _ ] => clear H adamc@118: end. adamc@256: adamc@262: Ltac guess v H := adamc@256: repeat match type of H with adamc@256: | forall x : ?T, _ => adamc@256: match type of T with adamc@256: | Prop => adamc@256: (let H' := fresh "H'" in adamc@256: assert (H' : T); [ adamc@262: solve [ eauto 6 ] adamc@256: | generalize (H H'); clear H H'; intro H ]) adamc@256: || fail 1 adamc@256: | _ => adamc@262: (generalize (H v); clear H; intro H) adamc@262: || let x := fresh "x" in adamc@256: evar (x : T); adamc@256: let x' := eval cbv delta [x] in x in adamc@256: clear x; generalize (H x'); clear H; intro H adamc@256: end adamc@256: end. adamc@256: adamc@262: Ltac guessKeep v H := adamc@256: let H' := fresh "H'" in adamc@262: generalize H; intro H'; guess v H'.