blob: f09b27c2b1ca2b133059f2cd4bcaba382783dc1d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
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.
|
