Squashed vs constructive proofs

Here's a small code sample showing how to move between squash and constructive proofs (thanks to Arvind Arasu, who prompted this discussion)

See WorkingWithSquashedProofs.fst

What follows is a stub, left as a reminder that new F* users are often confused by the difference between squashed and constructive proofs, and have trouble understanding the differences.

petercommand [11:58 AM]
Seems that == is the squashed equals type, but filling in Refl for the term doesn’t work
catalin-hritcu [2 days ago]
building a fully explicit proof term is generally quite painful in F*

petercommand [Oct 23rd at 1:45 PM]
is there any documents on type squashing?

2 replies
catalin-hritcu [1 day ago]
Not much beyond the code itself

petercommand [1 day ago]
Ah..ok thanks!

AHan [Today at 12:09 PM]
Hello, We are trying to prove there existence of left inverse from right identity and right inverse
And somehow we are stuck at the last step , don't know what term (  of type `Group?.op gp y x == Group?.u gp))`  ) we should return...
Is there any better way to find out the term?
https://gist.github.com/potsrevennil/1485a5b7b0ebc8d9a24b1a5000fd23c8#file-test-fst-L27 (edited)


13 replies
catalin-hritcu [1 hour ago]
In general, you should only use cexists for proofs you want to do fully constructively.


catalin-hritcu [1 hour ago]
In this case the == is a squashed equality, so can simply be a post-condition:
```val left_inv: #a:Type -> gp: group a -> x:a ->
  Pure a (requires True) (ensures fun y -> Group?.op gp y x == Group?.u gp)
let left_inv #a gp x =
  let right_inv = Group?.inverse gp in
  let right_id = Group?.identity gp in
  let assoc = Group?.associativity gp in
  let ExIntro y p = right_inv x in
  right_id y;
  assoc y x y;
  y```


catalin-hritcu [1 hour ago]
Now this still fails, because you still need to convince F* that this post-condition holds


catalin-hritcu [38 minutes ago]
This kind of proofs will get easier once support for "calculational proofs" gets mainlined: https://github.com/FStarLang/FStar/issues/1549
https://github.com/FStarLang/FStar/issues/1522#issuecomment-425988450


catalin-hritcu [38 minutes ago]
In the meanwhile you can add "assert" statements to see how far F* can get with the proof


AHan [32 minutes ago]
OK! Thank you very much!


catalin-hritcu [31 minutes ago]
Another thing you can do is stare at the proof goal using tactics; in your original code you can do
  ```ExIntro y (synth_by_tactic (fun () -> dump "debugging point" ; admit_all()))```
to see your proof goal


catalin-hritcu [29 minutes ago]
or if you move the equality to the postcondition (as I proposed above), then you would do:
  ```assert(Group?.op gp y x == Group?.u gp) by
    (dump "debugging point" ; admit_all());
  y```


AHan [26 minutes ago]
Thanks a lot!
Btw, I'm still not quite understand when is it suitable to use cexist ?


catalin-hritcu [24 minutes ago]
In the orignal code I pointed you: https://github.com/FStarLang/FStar/blob/master/examples/metatheory/LambdaOmega.fst#L461
`cexists` is used with `step` which is an inductive relation, so inherently constructive (as opposed to squashed)


catalin-hritcu [23 minutes ago]
for such constructive propositions one has to provide an explicit proof term witness, either manually or using synth_by_tactic (edited)


catalin-hritcu [23 minutes ago]
for squashed things one by default relies on the SMT solver (which produces no witness), although often it needs help too, in the form of lemmas you apply, or assert <proposition> [by <tactic>] ... (edited)


AHan [4 minutes ago]
What does the constructive stands for here ? And why is it opposed to squash?