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@59: match goal with adamc@59: | [ H : ex _ |- _ ] => destruct H adamc@59: adamc@51: | [ H : ?F _ = ?F _ |- _ ] => injection H; adamc@51: match goal with 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@66: | [ H : ?F _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst adamc@66: | [ H : ?F _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst adamc@84: | [ H : ?F _ _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst adamc@84: | [ H : ?F _ _ _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst adamc@84: | [ H : ?F _ _ _ _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst adamc@50: end. adamc@50: adamc@2: Ltac rewriteHyp := adamc@2: match goal with adamc@2: | [ H : _ |- _ ] => rewrite H 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@86: Ltac crush'' tryLemmas lemmas invOne := adamc@66: let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence adamc@59: in (sintuition; rewriter; adamc@86: match tryLemmas with adamc@86: | true => repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L)); adamc@86: repeat (simplHyp invOne; intuition)); un_done adamc@86: | _ => idtac adamc@86: end; sintuition; try omega; try (elimtype False; omega)). adamc@59: adamc@86: Ltac crush := crush'' false tt fail. adamc@86: Ltac crush' := crush'' true. 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@85: | _ _ ?A => doit A adamc@85: | _ ?A => doit A adamc@85: end.