blob: 4f17f081b4494fd8b14bc3140812220bcd6d4ae0 (
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
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* $Id: *)
Require Export Equality.
Declare ML Module "Inv" "Leminv".
Syntax tactic level 0:
| inversion [<<(Inv $ic $id)>>] -> [ (INVCOM $ic) [1 1] $id]
| inversion_in [<<(InvIn $ic $id ($LIST $l))>>]
-> [ (INVCOM $ic) [1 1] $id (CLAUSE ($LIST $l))]
| dep_inv [<<(DInv $ic $id)>>] -> ["Dependent " (INVCOM $ic) [1 1] $id]
| dep_inv_with [<<(DInvWith $ic $id $c)>>]
-> ["Dependent " (INVCOM $ic) [1 1] $id [1 1] "with " $c]
(* Use rules *)
| inv_using
[<<(UseInversionLemma $id $c)>>] -> ["Inversion " $id [1 1] "using " $c]
| inv_using_in [<<(UseInversionLemmaIn $id $c ($LIST $l))>>]
-> ["Inversion " $id [1 1] "using " $c (CLAUSE ($LIST $l))]
| simple_inv [<<(INVCOM "HalfInversion")>>] -> [ "Simple Inversion" ]
| inversion_com [<<(INVCOM "Inversion")>>] -> [ "Inversion" ]
| inversion_clear [<<(INVCOM "InversionClear")>>] -> [ "Inversion_clear" ].
Grammar tactic simple_tactic: ast :=
inversion [ inversion_com($ic) identarg($id) ] -> [(Inv $ic $id)]
| inversion_num [ inversion_com($ic) pure_numarg($n) ] -> [(Inv $ic $n)]
| inversion_in [ inversion_com($ic) identarg($id) "in" ne_identarg_list($l) ]
-> [(InvIn $ic $id ($LIST $l))]
| dep_inv [ "Dependent" inversion_com($ic) identarg($id)] -> [(DInv $ic $id)]
| dep_inv_num [ "Dependent" inversion_com($ic) pure_numarg($n) ] -> [(DInv $ic $n)]
| dep_inv_with
[ "Dependent" inversion_com($ic) identarg($id) "with" constrarg($c) ]
-> [(DInvWith $ic $id $c) ]
| dep_inv_num_with
[ "Dependent" inversion_com($ic) pure_numarg($n) "with" constrarg($c) ]
-> [(DInvWith $ic $n $c) ]
| inv_using [ inversion_com($ic) identarg($id) "using" constrarg($c) ]
-> case [$ic] of
"Inversion" -> [(UseInversionLemma $id $c)]
esac
| inv_num_using [ inversion_com($ic) pure_numarg($n) "using" constrarg($c) ]
-> case [$ic] of
Inversion -> [(UseInversionLemma $n $c)]
esac
| inv_using_in
[ inversion_com($ic) identarg($id) "using" constrarg($c)
"in" ne_identarg_list($l) ]
-> case [$ic] of
"Inversion" -> [(UseInversionLemmaIn $id $c ($LIST $l))]
esac
with inversion_com: ast :=
simple_inv [ "Simple" "Inversion" ] -> [ "HalfInversion" ]
| inversion_com [ "Inversion" ] -> [ "Inversion" ]
| inv_clear [ "Inversion_clear" ] -> [ "InversionClear" ].
Grammar vernac vernac: ast :=
der_inv_clr [ "Derive" "Inversion_clear" identarg($na) identarg($id) "." ]
-> [(MakeInversionLemmaFromHyp 1 $na $id)]
| der_inv_clr_num [ "Derive" "Inversion_clear"
numarg($n) identarg($na) identarg($id) "." ]
-> [(MakeInversionLemmaFromHyp $n $na $id)]
| der_inv_clr_with_srt [ "Derive" "Inversion_clear" identarg($na)
"with" constrarg($com) "Sort" sortarg($s) "." ]
-> [(MakeInversionLemma $na $com $s)]
| der_inv_clr_with [ "Derive" "Inversion_clear" identarg($na)
"with" constrarg($com) "." ]
-> [(MakeInversionLemma $na $com (CONSTR (PROP))) ]
| der_inv_with_srt [ "Derive" "Inversion" identarg($na)
"with" constrarg($com) "Sort" sortarg($s) "." ]
-> [(MakeSemiInversionLemma $na $com $s)]
| der_inv_with [ "Derive" "Inversion" identarg($na) "with" constrarg($com) "." ]
-> [(MakeSemiInversionLemma $na $com (CONSTR (PROP)))]
| der_inv [ "Derive" "Inversion" identarg($na) identarg($id) "." ]
-> [(MakeSemiInversionLemmaFromHyp 1 $na $id)]
| der_inv_num [ "Derive" "Inversion"
numarg($n) identarg($na) identarg($id) "." ]
-> [(MakeSemiInversionLemmaFromHyp $n $na $id)]
| der_dep_inv_with_srt [ "Derive" "Dependent" "Inversion" identarg($na)
"with" constrarg($com) "Sort" sortarg($s) "." ]
-> [(MakeDependentSemiInversionLemma $na $com $s)]
| der_dep_inv_clr_with_srt
[ "Derive" "Dependent" "Inversion_clear" identarg($na)
"with" constrarg($com) "Sort" sortarg($s)"." ]
-> [(MakeDependentInversionLemma $na $com $s)].
|
