In proof mode, if I know an expression e of type T, I can write pose foo : T := e to add foo := e : T as a hypothesis. Often, I don't care about that foo is the same as e, I only care that foo has type T, so in the hypotheses list I would like to see foo : T instead of foo := e : T to reduce mental clutter. How can I do that?
$\begingroup$
$\endgroup$
5
3 Answers
$\begingroup$
$\endgroup$
answered Feb 19, 2022 at 21:07
$\begingroup$
$\endgroup$
assert was already mentioned in another answer. An alternative (if you like the word pose) is pose proof. Several syntax variants are supported, including the one with :=. In practice, the two will produce exactly the same proof, so this is a purely stylistic choice.
$\begingroup$
$\endgroup$
The question text did not make that clear, but it turns out (from the comments) that what you are using is actually the pose tactic from SSReflect (documentation here) and not the standard Coq pose tactic (documentation here). If you want to keep using SSReflect tactics, then the recommended answer to your question is to replace pose with have (documentation here) when you do not need the body. E.g.:
Require Import ssreflect.
Lemma foo S T (f : S -> T) (s : S) : T.
Proof.
have foo : T := f s.
:if I usepose foo : T := t1. Butpose (foo := t1)works here. $\endgroup$Lemma foo S T (f : S -> T) (s : S) : T. Proof. pose foo : T := f s.$\endgroup$From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.and then it'll work. $\endgroup$