3 ms·

I can't tell if this is pseudocode or what proof in coq usually looks like: Theorem NestedTreeContains1: forall (t: tree), t = Node example 2 (Node Nil

I can't tell if this is pseudocode or what proof in coq usually looks like: Theorem NestedTreeContains1: forall (t: tree), t = Node example 2 (Node Nil 3 Nil) -> contains 1 t = true. Proof. nail. wreck t. - wat. - wreck H into Ht1, Hv and Ht2. sub Hv. evaluate. sub Ht1. just ExampleTreeContains1. Qed. Theorem, forall, qed look fairly likely. Are there built-in operations in coq called 'wat' and 'wreck'?

Smaug123 3y ago
They are not built-in, no. https://github.com/awalterschulze/ccc-talk/blob/1e781326d2e3c372b6d49bc2f6ff5737dc6757d8/Coq/src/BST/ConstructionToolbox.v#L24 https://github.com/awalterschulze/ccc-talk/blob/1e781326d2e3...
legobmw99 3y ago
I used Coq in one class in school, and I never encountered wat or wreck. It’s possible they’re user- or library-defined tactics. One thing I think is important about Coq is that it really is meant to be interactive. Even after a fair amount of usage I still find it somewhat tricky to just read a proof, especially a nontrivial one. A good IDE will show you a panel that includes all your hypothesis and requirements so far, updating as you run each line
082349872349872 3y ago
A cursory search reveals they're not builtin, but were written for the talk: https://github.com/awalterschulze/ccc-talk/blob/main/Coq/src/BST/ConstructionToolbox.v https://github.com/awalterschulze/ccc-talk/blob/main/Coq/src... nail ~= intros wat ~= discriminate etc.
- colonwqbang 3y ago
  "wreck" is actually "destruct", "same" is "reflexivity"... It boggles the mind why the author would make up fanciful new names for the fundamental tactics in this "how to" article.
  - 21eleven 3y ago
    He's giving a talk, it's for the lulz If you are giving a talk on a theorem proving programing language you're gonna want to make it fun
- thaliaarchi 3y ago
  The only useful ltac I see in there is compare, which can save a lot of tedious rewrites, when needing that frequently.
ekidd 3y ago
As other people note, a lot of those seem to be local aliases defined by the author. But the most important thing to understand about Coq is that it's meant to be read in an IDE. The IDE will show you, at each step, what has been proved and what remains to be proved. The "tactics" you see above basically mean, "At this point in the proof, we can make progress by substituting Hv. And in context, this will make sense. But without being able to see the proof state at each step, Coq can be incredibly cryptic.

Smaug123 3y ago

They are not built-in, no. https://github.com/awalterschulze/ccc-talk/blob/1e781326d2e3c372b6d49bc2f6ff5737dc6757d8/Coq/src/BST/ConstructionToolbox.v#L24 https://github.com/awalterschulze/ccc-talk/blob/1e781326d2e3...

legobmw99 3y ago

I used Coq in one class in school, and I never encountered wat or wreck. It’s possible they’re user- or library-defined tactics. One thing I think is important about Coq is that it really is meant to be interactive. Even after a fair amount of usage I still find it somewhat tricky to just read a proof, especially a nontrivial one. A good IDE will show you a panel that includes all your hypothesis and requirements so far, updating as you run each line

082349872349872 3y ago

A cursory search reveals they're not builtin, but were written for the talk: https://github.com/awalterschulze/ccc-talk/blob/main/Coq/src/BST/ConstructionToolbox.v https://github.com/awalterschulze/ccc-talk/blob/main/Coq/src... nail ~= intros wat ~= discriminate etc.

colonwqbang 3y ago
"wreck" is actually "destruct", "same" is "reflexivity"... It boggles the mind why the author would make up fanciful new names for the fundamental tactics in this "how to" article.
- 21eleven 3y ago
  He's giving a talk, it's for the lulz If you are giving a talk on a theorem proving programing language you're gonna want to make it fun
thaliaarchi 3y ago
The only useful ltac I see in there is compare, which can save a lot of tedious rewrites, when needing that frequently.

ekidd 3y ago

As other people note, a lot of those seem to be local aliases defined by the author. But the most important thing to understand about Coq is that it's meant to be read in an IDE. The IDE will show you, at each step, what has been proved and what remains to be proved. The "tactics" you see above basically mean, "At this point in the proof, we can make progress by substituting Hv. And in context, this will make sense. But without being able to see the proof state at each step, Coq can be incredibly cryptic.