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
1 vote
1 answer
41 views

Coq ssreflect - rewrite inside \big

I'm trying to prove the following lemma : ...
  • 13
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: ...
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