Questions tagged [tactic]
A tactic is a command or instruction for constructing a formal proof by applying a common proof technique. For questions about high-level techniques for constructing proofs, use the tag (strategy).
39
questions
1
vote
1
answer
26
views
Feeding rewrites and other hints into an omnibus tactic
How do I feed rewrites that I've marked as safe into a custom tactic?
I'm trying to write shorter Coq proofs with more of the easy stuff hidden. To that end, in the script below I proved that ...
- 3,073
0
votes
1
answer
53
views
Coq equivalent of Lean's `nth_rewrite`
Does Coq have an equivalent of Lean's nth_rewrite? rewrite ... at ... appears to specialize at its first unification site ...
- 3,073
2
votes
1
answer
43
views
Coq cannot `simple apply reflexivity` in custom tactic
The fast reflexivity tactic shown below is very interesting. It exposes some of the unification machinery by disabling it.
I'm planning on going back and using it in the first part of Software ...
- 3,073
7
votes
2
answers
156
views
When is the lean 4 "by" required?
I am reading an introductory math/lean course here, and got confused about when the tactic/keyword by is required. It is used most of the time, but is occasionally ...
- 2,210
3
votes
1
answer
63
views
What's the idiomatic way to instantiate a tuple of evars in Ltac2?
Suppose that I have a local definition of a type ty in the context, and ty can be any nested tuple, e.g.:
...
- 33
0
votes
1
answer
60
views
Ltac, How to intro a fresh variable which may already have a good estiblished name given by a universal quantifier?
Context
I am currently self studying Coq following the Software Foundations book series which I am finding very approachable.
I have finally gotten round to ...
- 133
2
votes
1
answer
93
views
What does `induction ... in ...` do in Coq?
I'm self-studying the Semantics course, and met the following proof script in the warmup directory:
...
- 123
0
votes
1
answer
37
views
Tactic to Propify a bool expression
Let's say I have bool expressions <bexp> consisting of true, false, variables, ...
- 1,502
3
votes
2
answers
136
views
Lean4: How to construct an HEq between dependent functions?
I have an extremely simple goal to prove:
HEq
(fun px rd =>
match px, rd with
| Sum.inr _ppos, dir => dir)
fun x => id
The reason the match ...
- 41
3
votes
2
answers
69
views
Creating a tactic for 'destructing' a list by last element?
Sometimes, I have a context in which I have some l : list X, and I want to prove the goal by proving that (1) If l = [], the ...
- 1,502
2
votes
1
answer
94
views
Proving that equality is decidable on an ``Inductive Set``
I've managed to prove that equality within a type is indeed decidable.
...
- 191
4
votes
2
answers
185
views
Which proof assistants implement Church's rule?
Church's rule (CR) is one of the hallmarks of constructive mathematics, and is an admissible rule in a wide variety of constructive theories (you might consider CR to be a requirement for constructive ...
- 165
3
votes
1
answer
197
views
Selecting both a hypothesis and Goal while applying a tactic
I have a hypothesis H and some function foo. I want to simplify foo in both H and the ...
- 1,502
7
votes
1
answer
556
views
Examples of theories where tactic language is required for simple proofs
I was always under the impression, that separate tactic languages were generally considered to be vital for writing long proofs. I see tactic languages as a kind of interpreted DSL to generate ...
- 177
8
votes
1
answer
370
views
How does Lean `simp` tactic work?
The doc at https://leanprover-community.github.io/extras/simp.html says about simp:
all it does is repeatedly replace (or rewrite) subterms of the form A by B, for ...
- 313