Because F* uses an SMT solver in the backend, and in general SMT solvers cannot solve formulas by induction*. Literature on SAT/SMT is huge and I am not the right person to point you to the best reads but you can always start at wikipedia: https://en.wikipedia.org/wiki/Satisfiability_modulo_theories <https://en.wikipedia.org/wiki/Satisfiability_modulo_theories>
* Came by this paper recently, which tries to integrate inductive reasoning to the CVC4 solver: https://dl.acm.org/citation.cfm?id=2958791 > On Apr 3, 2018, at 3:12 AM, Nitin John Raj via fstar-club > <fstar-club@lists.gforge.inria.fr> wrote: > > Hey all! > I was practicing verifying lemmas in F* from the tutorial, and I came across > a few things that I didn't really understand. > > From > https://www.fstar-lang.org/tutorial/tutorial.html#sec-to-type-intrinsically-or-to-prove-lemmas > > <https://www.fstar-lang.org/tutorial/tutorial.html#sec-to-type-intrinsically-or-to-prove-lemmas>: > ''' > val reverse: #a:Type -> f:(list a -> Tot (list a)){forall l. l == f (f l) > However, F* refuses to accept this as a valid type for reverse: proving this > property requires two separate inductions, neither of which F* can perform > automatically. > > ''' > > Why can't F* perform these inductions automatically? What are the bounds of > inference on the SMT solver? Can someone shoot me resources on the same? > > Sincerely, > > Nitin John Raj > > _______________________________________________ > fstar-club mailing list > fstar-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
_______________________________________________ fstar-club mailing list fstar-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
