All Questions
25
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
0
votes
1
answer
55
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,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
3
votes
1
answer
64
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
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
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
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
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
1
answer
198
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
0
votes
1
answer
116
views
Specializing forall quantifiers in Coq
I have an inductively defined type of expressions:
...
4
votes
0
answers
64
views
Using CoqHammer from Ltac2
As it seems most likely to me, due to the special way arguments are evaluated in CoqHammer tactics (I tried to read the source code in OCaml but unfortunately I didn't understand much of it), it is ...
1
vote
1
answer
126
views
Rewriting inside quantified propositions in Coq?
Is there a simple way to use rewrites inside quantified Props? As an example, consider the following:
...
- 1,502
2
votes
1
answer
152
views
Debug autorewrite in Coq
I often meet proofs using autorewrite which Coq takes a while to process for some reason. (Setoid rewriting)
I then manually figure out which rewrite rules were ...
- 224
3
votes
3
answers
210
views
In Coq, is there a simpler tactic for introducing a disjunction and immediately destructing it?
Very often, I find myself writing some tactics like these:
assert (delta = 1 \/ delta <> 1) as Hd by lia.
destruct Hd.
...(proceed to work with two cases)...
...
- 1,502