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@160:     | [ H : ?F ?X = ?F ?Y |- _ ] => injection H;
adamc@51:       match goal with
adamc@160:         | [ |- F X = F Y -> _ ] => fail 1
adamc@85:         | [ |- _ = _ -> _ ] => try clear H; intros; try subst
adamc@51:       end
adamc@51:     | [ H : ?F _ _ = ?F _ _ |- _ ] => injection H;
adamc@51:       match goal with
adamc@85:         | [ |- _ = _ -> _ = _ -> _ ] => try clear H; intros; try subst
adamc@51:       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@85: Theorem dep_destruct : forall (T : Type) (T' : T -> Type) x (v : T' x) (P : T' x -> Prop),
adamc@85:   (forall x' (v' : T' x') (Heq : x' = x), P (match Heq in (_ = x) return (T' x) with
adamc@85:                                                | refl_equal => v'
adamc@85:                                              end))
adamc@85:   -> P v.
adamc@85:   intros.
adamc@85:   generalize (H _ v (refl_equal _)); trivial.
adamc@85: Qed.
adamc@85: 
adamc@85: Ltac dep_destruct E :=
adamc@85:   let doit A :=
adamc@85:     let T := type of A in
adamc@85:       generalize dependent E;
adamc@85:         let e := fresh "e" in
adamc@85:           intro e; pattern e;
adamc@85:             apply (@dep_destruct T);
adamc@85:               let x := fresh "x" with v := fresh "v"  in
adamc@85:                 intros x v; destruct v; crush;
adamc@85:                   let bestEffort Heq E tac :=
adamc@85:                     repeat match goal with
adamc@85:                              | [ H : context[E] |- _ ] =>
adamc@85:                                match H with
adamc@85:                                  | Heq => fail 1
adamc@85:                                  | _ => generalize dependent H
adamc@85:                                end
adamc@85:                            end;
adamc@85:                     generalize Heq; tac Heq; clear Heq; intro Heq;
adamc@85:                       rewrite (UIP_refl _ _ Heq); intros in
adamc@85:                   repeat match goal with
adamc@85:                            | [ Heq : ?X = ?X |- _ ] =>
adamc@85:                              generalize (UIP_refl _ _ Heq); intro; subst; clear Heq
adamc@85:                            | [ Heq : ?E = _ |- _ ] => bestEffort Heq E ltac:(fun E => rewrite E)
adamc@85:                            | [ Heq : _ = ?E |- _ ] => bestEffort Heq E ltac:(fun E => rewrite <- E)
adamc@85:                          end
adamc@85:                   in match type of E with
adamc@173:                        | _ ?A => doit A
adamc@85:                        | _ _ ?A => doit A
adamc@173:                        | _ _ _ ?A => doit A
adamc@85:                      end.
adamc@118: 
adamc@118: Ltac clear_all :=
adamc@118:   repeat match goal with
adamc@118:            | [ H : _ |- _ ] => clear H
adamc@118:          end.