All Questions
25
questions
11
votes
2
answers
415
views
Proving uniqueness of an instance of an indexed inductive type
Consider the simple indexed inductive type
Inductive Single : nat -> Set :=
| single_O : Single O
| single_S {n} : Single n -> Single (S n).
Intuitively, I ...
- 213
8
votes
2
answers
228
views
How to prove `forall m n : nat, m == n -> m = n`?
I am learning Coq with ssreflect. Just to understand things, I've proved forall a b : bool, a == b -> a = b but I can't figure out how to prove ...
- 317
6
votes
1
answer
405
views
How to evaluate proof terms through opaque definitions?
Is there is a way to force computation over opaque terms, for the purposes of debugging/meta-analysis of proof scripts.
I understand why Coq doesn’t do this by default, and guess it would probably ...
5
votes
1
answer
313
views
Cannot discriminate `0 = 1`
I am just practicing a bit with coq, doing some UniMath exercises and am trying to prove (0 = 1) -> empty. However, for some reason, I seem unable to reason ...
- 265
5
votes
0
answers
164
views
Prove equality in a record type
I am trying to prove something about monoids an categories. This results in the following (partial) proof:
...
- 265
4
votes
1
answer
175
views
Why does this trivial proof fail with structuring tacticals?
Given this:
Inductive color := Black | White.
Inductive point_state :=
| Occupied of color
| Empty
.
this works:
...
- 143
4
votes
0
answers
65
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 ...
3
votes
3
answers
213
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
3
votes
2
answers
74
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
3
votes
1
answer
156
views
Applying custom tactic in hypothesis
To avoid tedious repetition I have a tactic that looks something like this:
Ltac unfolds := try unfold foo;
try unfold bar;
try unfold baz;
apply some_lemma.
...
- 170
3
votes
1
answer
200
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
3
votes
2
answers
232
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
1
answer
66
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
3
votes
0
answers
93
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?
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