Questions tagged [coq-ssreflect]
ssreflect is a special set of tactics designed to enable small-scale reflection proof methodology in Coq proof assistant.
4
questions
4
votes
0
answers
49
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 ...
- 497
4
votes
1
answer
148
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
3
answers
65
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 <...
- 273
7
votes
2
answers
137
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 ...
- 273