Mentions légales du service

Skip to content
Snippets Groups Projects
Closed Variants for lemma functions
  • View options
  • Variants for lemma functions

  • View options
  • Closed Issue created by Guillaume Melquiond
    type nat = O | S nat
    
    let rec function plus (x y : nat) : nat =
      match x with
      | O -> y
      | S x' -> plus x' (S y)
      end
    
    let rec lemma plus_S (x y : nat) : unit
      variant { x }
    = match x with
      | O -> ()
      | S x' -> plus_S x' (S y)
      end

    Why3 rejects the let rec lemma definition if variant is not specified. It would be more user-friendly if it could use the same heuristic as for the let rec function definition. Moreover, that would avoid an especially dumb proof obligation:

    goal VC plus_S :
      forall x:nat.
      match x with
      | O -> true
      | S x' -> match x with
          | O -> false
          | S f -> f = x'
          end
      end

    Linked items ... 0

  • Activity

    • All activity
    • Comments only
    • History only
    • Newest first
    • Oldest first
    Loading Loading Loading Loading Loading Loading Loading Loading Loading Loading