• Jean-Christophe Filliatre's avatar
    new VC to prove well-foundedness of user-provided variants · 4af9081d
    Jean-Christophe Filliatre authored
    fixes issue #57
    
    a new theory relations.WellFounded is introduced for this purpose
    (and must be imported whenever one wants to make use of a custom
    relation for a variant)
    
    it defines, inductively, a notion of accessibility for a given
    predicate R (x is accessible whenever all elements smaller than x for R
    are alreay accessible)
    
    whenever one has to prove that a variant decreases, a new VC is also
    generated, to show that the old value of the variant is accessible
    for the order relation
    
    note: accessibility being defined inductively, proving well-foundedness
    is out of reach of SMT solvers; but at least this is sound now
    4af9081d
tortoise_and_hare_WP_TortoiseAndHare_WP_parameter_tortoise_hare_1.v 4.32 KB