Menu
I'm a new user for Coq. I have defined some functions:
Definition p (a : nat) := (a + 1, a + 2, a + 3).
Definition q :=
let (s, r, t) := p 1 in
s + r + t.
Definition q' :=
match p 1 with
| (s, r, t) => s + r + t
end.
I'm trying to destruct the result of p into a tuple representation. However coqc complains on q:
Error: Destructing let on this type expects 2 variables.
while q' can pass the compilation. If I change p to return a pair(a + 1, a + 2), the corresponding q and q' both work fine.
Why let-destruct only allows pair? Or have I made any error in syntax? I've checked with Coq manual but found no clue.
Thank you!
890
You can use Fail Fail Qed. to really assert that a proof is complete, including doing universe checks, but then still be able to Restart it. I think this is only useful for illustrating small examples but it's amusing that it works. (The new Succeed vernacular in Coq 8.15 is a better replacement, because it preserves error messages on failure.)
Note that this isn't the best plan because you end up with transparent proofs, which isn't great; ideally Coq would just support Theorem foo := syntax for opaque proofs. Haskell has an operator f $ x, which is the same as f x except that its parsed differently: f $ 1 + 1 means f (1 + 1), avoiding parentheses.
Tactics specify how to transform the proof state of an incomplete proof to eventually generate a complete proof. Proofs can be developed in two basic ways: In forward reasoning , the proof begins by proving simple statements that are then combined to prove the theorem statement as the last step of the proof.
You can also use intros to introduce all propositions on the left side of an implication as assumptions. If intros is used by itself, Coq will introduce all the variables and hypotheses that it can, and it will assign names to them automatically. You can provide your own names (or introduce fewer things) by supplying those names in order.
What is a bit confusing in Coq is that there are two different forms of destructing let. The one you are looking for needs a quote before the pattern:
Definition p (a : nat) := (a + 1, a + 2, a + 3).
Definition q :=
let '(s, r, t) := p 1 in
s + r + t.
Prefixing the pattern with a quote allows you to use nested patterns and use user-defined notations in them. The form without the quote only works with one-level patterns, and doesn't allow you to use notations, or refer to constructor names in your patterns.
120
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
