diff options
Diffstat (limited to 'test-suite/bugs/closed/4644.v')
-rw-r--r-- | test-suite/bugs/closed/4644.v | 52 |
1 files changed, 52 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4644.v b/test-suite/bugs/closed/4644.v new file mode 100644 index 00000000..f09b27c2 --- /dev/null +++ b/test-suite/bugs/closed/4644.v @@ -0,0 +1,52 @@ +(* Testing a regression of unification in 8.5 in problems of the form + "match ?y with ... end = ?x args" *) + +Lemma foo : exists b, forall a, match a with tt => tt end = b a. +Proof. +eexists. intro. +refine (_ : _ = match _ with tt => _ end). +refine eq_refl. +Qed. + +(**********************************************************************) + +Axiom proof_admitted : False. +Tactic Notation "admit" := case proof_admitted. +Require Export Coq.Classes.Morphisms. +Require Import Coq.Lists.List. + +Global Set Implicit Arguments. + +Definition list_caset A (P : list A -> Type) (N : P nil) (C : forall x xs, P (x::xs)) + ls + : P ls + := match ls with + | nil => N + | x::xs => C x xs + end. + +Axiom list_caset_Proper' + : forall {A P}, + Proper (eq + ==> pointwise_relation _ (pointwise_relation _ eq) + ==> eq + ==> eq) + (@list_caset A (fun _ => P)). +Goal forall (T T' : Set) (a3 : list T), exists y2, forall (a4 : T' -> bool), + match a3 with + | nil => 0 + | (_ :: _)%list => 1 + end = y2 a4. + clear; eexists; intros. + reflexivity. Undo. + Local Ltac t := + lazymatch goal with + | [ |- match ?v with nil => ?N | cons x xs => @?C x xs end = _ :> ?P ] + => let T := type of v in + let A := match (eval hnf in T) with list ?A => A end in + refine (@list_caset_Proper' A P _ _ _ _ _ _ _ _ _ + : @list_caset A (fun _ => P) N C v = match _ with nil => _ | cons x xs => _ end) + end. + (etransitivity; [ t | reflexivity ]) || fail 0 "too early". + Undo. + t. |