diff options
| -rw-r--r-- | test-suite/success/dependentind.v | 7 | ||||
| -rw-r--r-- | theories/Program/Equality.v | 26 |
2 files changed, 25 insertions, 8 deletions
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v index fe0165d08..70fb75888 100644 --- a/test-suite/success/dependentind.v +++ b/test-suite/success/dependentind.v @@ -1,5 +1,11 @@ Require Import Coq.Program.Program Coq.Program.Equality. +Goal forall (H: forall n m : nat, n = m -> n = 0) x, x = tt. +intros. +dependent destruction x. +reflexivity. +Qed. + Variable A : Set. Inductive vector : nat -> Type := vnil : vector 0 | vcons : A -> forall {n}, vector n -> vector (S n). @@ -84,6 +90,7 @@ Proof with simpl in * ; eqns ; eauto with lambda. intro. eapply app... Defined. + Lemma exchange : forall Γ Δ α β τ, term (Γ, α, β ; Δ) τ -> term (Γ, β, α ; Δ) τ. Proof with simpl in * ; eqns ; eauto. intros until 1. diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 06ff7cd10..d9d0073be 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -28,7 +28,7 @@ Hint Extern 10 => is_ground_goal ; progress exfalso : exfalso. Definition block {A : Type} (a : A) := a. Ltac block_goal := match goal with [ |- ?T ] => change (block T) end. -Ltac unblock_goal := cbv beta delta [block]. +Ltac unblock_goal := unfold block in *. (** Notation for heterogenous equality. *) @@ -214,7 +214,8 @@ Ltac simplify_eqs := Ltac simplify_IH_hyps := repeat match goal with - | [ hyp : _ |- _ ] => specialize_eqs hyp + | [ hyp : context [ block _ ] |- _ ] => + specialize_eqs hyp end. (** We split substitution tactics in the two directions depending on which @@ -377,14 +378,23 @@ Ltac is_introduced H := end. Tactic Notation "intro_block" hyp(H) := - (is_introduced H ; block_goal ; revert_until H) || + (is_introduced H ; block_goal ; revert_until H ; block_goal) || (let H' := fresh H in intros until H' ; block_goal) || (intros ; block_goal). Tactic Notation "intro_block_id" ident(H) := - (is_introduced H ; block_goal ; revert_until H) || + (is_introduced H ; block_goal ; revert_until H; block_goal) || (let H' := fresh H in intros until H' ; block_goal) || (intros ; block_goal). -Ltac simpl_dep_elim := simplify_dep_elim ; simplify_IH_hyps ; unblock_goal. +Ltac unblock_dep_elim := + match goal with + | |- block ?T => + match T with context [ block _ ] => + unfold block at 1 ; intros ; unblock_goal + end + | _ => unblock_goal + end. + +Ltac simpl_dep_elim := simplify_dep_elim ; simplify_IH_hyps ; unblock_dep_elim. Ltac do_intros H := (try intros until H) ; (intro_block_id H || intro_block H). @@ -395,7 +405,7 @@ Ltac do_depelim tac H := do_depelim_nosimpl tac H ; simpl_dep_elim. Ltac do_depind tac H := (try intros until H) ; intro_block H ; - generalize_eqs_vars H ; tac H ; simplify_dep_elim ; simplify_IH_hyps ; unblock_goal. + generalize_eqs_vars H ; tac H ; simpl_dep_elim. (** To dependent elimination on some hyp. *) @@ -412,8 +422,8 @@ Ltac depind id := do_depind ltac:(fun hyp => do_ind hyp) id. (** A variant where generalized variables should be given by the user. *) Ltac do_depelim' rev tac H := - (try intros until H) ; block_goal ; rev H ; generalize_eqs H ; tac H ; simplify_dep_elim ; - simplify_IH_hyps ; unblock_goal. + (try intros until H) ; block_goal ; rev H ; + (try revert_until H ; block_goal) ; generalize_eqs H ; tac H ; simpl_dep_elim. (** Calls [destruct] on the generalized hypothesis, results should be similar to inversion. By default, we don't try to generalize the hyp by its variable indices. *) |