Questions tagged [coq-ssreflect]
ssreflect is a special set of tactics designed to enable small-scale reflection proof methodology in Coq proof assistant.
5
questions
1
vote
1
answer
41
views
7
votes
1
answer
95
views
Tactic unification vs evarconv in Coq
I gather, from practical experience and Zulip hearsay, that Coq has two unification algorithms, known as “tactic unification” and “evarconv”. However, I can't find any documentation on these from a ...
- 601
4
votes
1
answer
158
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
5
votes
3
answers
81
views
Hide the value of a hypothesis introduced by `pose`, show only its type
In proof mode, if I know an expression e of type T, I can write pose foo : T := e to add <...
- 317
8
votes
2
answers
160
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