Hi Pedro: You could prove this lemma by providing squashed `Val_big_step v` as a proof of `big_step (EVal v) v`. We need to squash `Val_big_step v` since lemmas (and refinements, pre- and postconditions etc.) fall into the classical, proof-irrelevant fragment of F*. So here is then one way to prove the lemma:
``` assume val value : eqtype type expr = | EVal : value -> expr type big_step : expr -> value -> Type = | Val_big_step : v:value -> big_step (EVal v) v let big_step_eval' () : Lemma (forall v. big_step (EVal v) v) = introduce forall v. big_step (EVal v) v with FStar.Squash.return_squash (Val_big_step v) ``` You can see more examples of such proofs here: https://github.com/FStarLang/FStar/blob/master/tests/micro-benchmarks/ClassicalSugar.fst. You may also want to checkout the `FStar.Classical` and `FStar.Squash` libraries in F* `ulib` (the `introduce ... with ...` syntax desugars to combinators in these libraries). Please let us know if you have more questions, -Aseem. From: Pedro Barroso <p.barr...@campus.fct.unl.pt> Sent: 15 October 2021 20:38 To: Aseem Rastogi <ase...@microsoft.com> Cc: fstar-club@lists.gforge.inria.fr Subject: Re: [EXTERNAL] [fstar-club] [Help] Inductive predicates Hi, thanks for your reply! Sorry to bother you again, I was able to define the relation with the example you provided. type big_step : expr -> value -> Type = | Val_big_step : v: value -> big_step (EVal v) v (...) Now I'm trying to prove this straightforward lemma: let big_step_eval () : Lemma (forall v. big_step (EVal v) v) = () Might be ignorance but I can't seem to find the proper way to prove this lemma. I'm used to doing these types of proofs in Why3. This lemma, for instance, is automatically proved in Why3. Furthermore, in Why3 it is just a matter of instantiating the rules of the inductive predicate (i.e. Val_big_step), but I don't know how to do this in F*. Thank you for your assistance, Pedro Aseem Rastogi <ase...@microsoft.com<mailto:ase...@microsoft.com>> escreveu no dia sexta, 8/10/2021 à(s) 08:37: Hi Pedro: It is possible to define these relations in F* using inductive predicates. See this for an example: https://github.com/FStarLang/FStar/blob/master/examples/metatheory/LambdaOmega.fst#L307<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2FFStarLang%2FFStar%2Fblob%2Fmaster%2Fexamples%2Fmetatheory%2FLambdaOmega.fst%23L307&data=04%7C01%7Caseemr%40microsoft.com%7Cb6ecd5c42d504548b13508d98fed9172%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637699072810780195%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=O6jwH%2FVLYNRZSahSHHj5a40MKgxhiqpRCU1Bn6VVIFQ%3D&reserved=0> Hope this helps, -Aseem. From: fstar-club <fstar-club-boun...@lists.gforge.inria.fr<mailto:fstar-club-boun...@lists.gforge.inria.fr>> On Behalf Of Pedro Barroso via fstar-club Sent: 07 October 2021 20:25 To: fstar-club@lists.gforge.inria.fr<mailto:fstar-club@lists.gforge.inria.fr> Subject: [EXTERNAL] [fstar-club] [Help] Inductive predicates Hello, good afternoon I'm doing an exercise of deeply embedding a language in F* and I'm wondering what is the idiomatic way to implement a big step semantics relation. How can we define a relation over a specific set? I saw the examples in https://fstar-lang.org/oplss2021/<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Ffstar-lang.org%2Foplss2021%2F&data=04%7C01%7Caseemr%40microsoft.com%7Cb6ecd5c42d504548b13508d98fed9172%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637699072810790149%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=0A2MQ%2FilEurzOIs9P3VKUYw13LaCmP45PQrCyf%2BGFO4%3D&reserved=0>, however, they implemented it with an interpreter with fuel. Is it possible to implement relations close to what we do in Coq, using Inductive predicates? Thank you for your assistance in this matter, Pedro -- Pedro
_______________________________________________ fstar-club mailing list fstar-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
