All Questions
6
questions
1
vote
1
answer
27
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,095
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,095
2
votes
1
answer
95
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
2
votes
1
answer
95
views
Proving that equality is decidable on an ``Inductive Set``
I've managed to prove that equality within a type is indeed decidable.
...
- 191
3
votes
2
answers
231
views
Coq: can `tauto` be used to prove classical tautologies?
When I experiment, I get inconsistent results.
Running the following code (with a proof included to double-check that it's provable)
...
3
votes
0
answers
92
views
Where is the discriminate tactic defined in Coq?
One can read the Coq documentation about discriminate tactic here.
Were is this tactic actually defined?
