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> 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 > > > > Hope this helps, > > > > -Aseem. > > > > *From:* fstar-club <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 > *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%7C2610d38281a94fcada9208d98a2a9b9d%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637692737920773631%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=0EK1N2YQ6vKHzPFHWcuowqZ4aEy9tNN74v0TXTvVU3I%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
