Questions tagged [coq-ssreflect]

ssreflect is a special set of tactics designed to enable small-scale reflection proof methodology in Coq proof assistant.

Filter by
Sorted by
Tagged with
4 votes
0 answers

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 ...
user avatar
  • 497
4 votes
1 answer

Why does this trivial proof fail with structuring tacticals?

Given this: Inductive color := Black | White. Inductive point_state := | Occupied of color | Empty . this works: ...
user avatar
4 votes
3 answers

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 <...
user avatar
  • 273
7 votes
2 answers

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 ...
user avatar
  • 273