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
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** Tactics related to subsets and proof irrelevance. *)
Require Import Coq.Program.Utils.
Require Import Coq.Program.Equality.
Require Export ProofIrrelevance.
Local Open Scope program_scope.
(** The following tactics implement a poor-man's solution for proof-irrelevance: it tries to
factorize every proof of the same proposition in a goal so that equality of such proofs becomes trivial. *)
Ltac on_subset_proof_aux tac T :=
match T with
| context [ exist ?P _ ?p ] => try on_subset_proof_aux tac P ; tac p
end.
Ltac on_subset_proof tac :=
match goal with
[ |- ?T ] => on_subset_proof_aux tac T
end.
Ltac abstract_any_hyp H' p :=
match type of p with
?X =>
match goal with
| [ H : X |- _ ] => fail 1
| _ => set (H':=p) ; try (change p with H') ; clearbody H'
end
end.
Ltac abstract_subset_proof :=
on_subset_proof ltac:(fun p => let H := fresh "eqH" in abstract_any_hyp H p ; simpl in H).
Ltac abstract_subset_proofs := repeat abstract_subset_proof.
Ltac pi_subset_proof_hyp p :=
match type of p with
?X =>
match goal with
| [ H : X |- _ ] =>
match p with
| H => fail 2
| _ => rewrite (proof_irrelevance X p H)
end
| _ => fail " No hypothesis with same type "
end
end.
Ltac pi_subset_proof := on_subset_proof pi_subset_proof_hyp.
Ltac pi_subset_proofs := repeat pi_subset_proof.
(** The two preceding tactics in sequence. *)
Ltac clear_subset_proofs :=
abstract_subset_proofs ; simpl in * |- ; pi_subset_proofs ; clear_dups.
Ltac pi := repeat f_equal ; apply proof_irrelevance.
Lemma subset_eq : forall A (P : A -> Prop) (n m : sig P), n = m <-> `n = `m.
Proof.
intros A P n m.
destruct n as (x,p).
destruct m as (x',p').
simpl.
split ; intros H ; subst.
- inversion H.
reflexivity.
- pi.
Qed.
(* Somewhat trivial definition, but not unfolded automatically hence we can match on [match_eq ?A ?B ?x ?f]
in tactics. *)
Definition match_eq (A B : Type) (x : A) (fn : {y : A | y = x} -> B) : B :=
fn (exist _ x eq_refl).
(* This is what we want to be able to do: replace the originally matched object by a new,
propositionally equal one. If [fn] works on [x] it should work on any [y | y = x]. *)
Lemma match_eq_rewrite : forall (A B : Type) (x : A) (fn : {y : A | y = x} -> B)
(y : {y:A | y = x}),
match_eq A B x fn = fn y.
Proof.
intros A B x fn y.
unfold match_eq.
f_equal.
destruct y.
(* uses proof-irrelevance *)
apply <- subset_eq.
symmetry. assumption.
Qed.
(** Now we make a tactic to be able to rewrite a term [t] which is applied to a [match_eq] using an arbitrary
equality [t = u], and [u] is now the subject of the [match]. *)
Ltac rewrite_match_eq H :=
match goal with
[ |- ?T ] =>
match T with
context [ match_eq ?A ?B ?t ?f ] =>
rewrite (match_eq_rewrite A B t f (exist _ _ (eq_sym H)))
end
end.
(** Otherwise we can simply unfold [match_eq] and the term trivially reduces to the original definition. *)
Ltac simpl_match_eq := unfold match_eq ; simpl.
|
