blob: c71db69952a3052a4edae01694abec114a334667 (
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
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
|
(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* Tactics for typeclass-based setoids.
*
* Author: Matthieu Sozeau
* Institution: LRI, CNRS UMR 8623 - Universit�copyright Paris Sud
* 91405 Orsay, France *)
(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
Require Export Coq.Classes.Relations.
Require Export Coq.Classes.Morphisms.
Set Implicit Arguments.
Unset Strict Implicit.
(** The setoid_replace tactics in Ltac, defined in terms of default relations [===def] and
the setoid_rewrite tactic. *)
Ltac setoidreplace H t :=
let Heq := fresh "Heq" in
cut(H) ; unfold default_relation ; [ intro Heq ; setoid_rewrite Heq ; clear Heq | t ].
Ltac setoidreplacein H H' t :=
let Heq := fresh "Heq" in
cut(H) ; unfold default_relation ; [ intro Heq ; setoid_rewrite Heq in H' ; clear Heq | t ].
Tactic Notation "setoid_replace" constr(x) "with" constr(y) :=
setoidreplace (x ===def y) idtac.
Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) :=
setoidreplacein (x ===def y) id idtac.
Tactic Notation "setoid_replace" constr(x) "with" constr(y) "by" tactic(t) :=
setoidreplace (x ===def y) ltac:t.
Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) "by" tactic(t) :=
setoidreplacein (x ===def y) id ltac:t.
Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) :=
setoidreplace (rel x y) idtac.
Tactic Notation "setoid_replace" constr(x) "with" constr(y)
"using" "relation" constr(rel) "by" tactic(t) :=
setoidreplace (rel x y) ltac:t.
Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id)
"using" "relation" constr(rel) :=
setoidreplacein (rel x y) id idtac.
Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id)
"using" "relation" constr(rel) "by" tactic(t) :=
setoidreplacein (rel x y) id ltac:t.
(** The [add_morphism_tactic] tactic is run at each [Add Morphism] command before giving the hand back
to the user to discharge the proof. It essentially amounts to unfold the right amount of [respectful] calls
and substitute leibniz equalities. One can redefine it using [Ltac add_morphism_tactic ::= t]. *)
Require Import Coq.Program.Tactics.
Ltac red_subst_eq_morphism concl :=
match concl with
| @Logic.eq ?A ==> ?R' => red ; intros ; subst ; red_subst_eq_morphism R'
| ?R ==> ?R' => red ; intros ; red_subst_eq_morphism R'
| _ => idtac
end.
Ltac destruct_morphism :=
match goal with
| [ |- @Morphism ?A ?R ?m ] => constructor
end.
Ltac reverse_arrows x :=
match x with
| @Logic.eq ?A ==> ?R' => revert_last ; reverse_arrows R'
| ?R ==> ?R' => do 3 revert_last ; reverse_arrows R'
| _ => idtac
end.
Ltac default_add_morphism_tactic :=
(try destruct_morphism) ;
match goal with
| [ |- (?x ==> ?y) _ _ ] => red_subst_eq_morphism (x ==> y) ; reverse_arrows (x ==> y)
end.
Ltac add_morphism_tactic := default_add_morphism_tactic.
|
