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'.