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)

module Sq
open FStar.Squash

//Suppose I have some predicates, it could be that inductive type about
//interleaving that you had
assume
val foo (a:Type) (x:a) : Type
assume
val bar (a:Type) (x:a) : Type

//And let's say I have a way of proving some Lemma based on a proof of this `pred`
assume
val foo_pf_implies_bar (a:Type) (x:a) (pf:foo a x)
  : Lemma (bar a x)

//Now, if I have `foo` in a refinement, I can still prove `bar, like so

//One can use FStar.Squash.bind_squash for that, but it takes a couple of steps

//expect_failure is an attribute that tells F* that this next definition will fail
[@expect_failure] //but this doesn't quite work because `bind_squash` expects a GTot function but we are giving it a Lemma, which isn't identical
let foo_implies_bar (a:Type) (x:a{foo a x})
  : Lemma (bar a x)
  = let s : squash (foo a x) = () in
    FStar.Squash.bind_squash #(foo a x) #(bar a x) s (foo_pf_implies_bar a x)

//So, to make it work, we need to turn a lemma into a GTot function returning a squash
let lemma_as_squash #a #b ($lem: (a -> Lemma b)) (x:a)
  : GTot (squash b)
  = lem x

//Now, I can use FStar.Squash.bind_squash to complete the proof
let foo_implies_bar (a:Type) (x:a{foo a x})
  : Lemma (bar a x)
  = FStar.Squash.bind_squash () (lemma_as_squash (foo_pf_implies_bar a x))

//Sorry, it's a bit bureaucractic and technical ... I wish this part of F* were simpler
//There's a bunch of redundancy between Lemma, squash, GTot, prop, etc.
//which is always confusing.

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?