examples/induction.mlw

   1
   2 (** Various ways of proving
   3
   4             p 0
   5             p 1
   6             forall n: int. 0 <= n -> p n -> p (n+2)
   7             ---------------------------------------
   8             forall n: int. 0 <= n -> p n
   9
  10     by induction using theories int.SimpleInduction or
  11     int.Induction or lemma functions.
  12
  13 *)
  14
  15 theory Hyps
  16   use export int.Int
  17
  18   predicate p int
  19
  20   axiom H0: p 0
  21   axiom H1: p 1
  22   axiom H2: forall n: int. 0 <= n -> p n -> p (n + 2)
  23
  24 end
  25
  26 (** {2 With a simple induction} *)
  27
  28 module Induction1
  29   use Hyps
  30
  31   predicate pr (k: int) = p k && p (k+1)
  32   clone int.SimpleInduction
  33     with predicate p = pr, lemma base, lemma induction_step
  34
  35   goal G: forall n: int. 0 <= n -> p n
  36
  37 end
  38
  39 (** {2 With a strong induction} *)
  40
  41 module Induction2
  42   use Hyps
  43
  44   clone int.Induction
  45     with predicate p = p, constant bound = zero
  46
  47   goal G: forall n: int. 0 <= n -> p n
  48
  49 end
  50
  51 (** {2 With a recursive lemma function} *)
  52
  53 module LemmaFunction1
  54   use Hyps
  55
  56   let rec lemma ind (n: int) requires { 0 <= n} ensures { p n }
  57     variant { n }
  58     = if n >= 2 then ind (n-2)
  59
  60   (** no need to write the following goal, that's just a check this is
  61       now proved *)
  62   goal G: forall n: int. 0 <= n -> p n
  63
  64 end
  65
  66 (** {2 With a while loop} *)
  67
  68 module LemmaFunction2
  69   use Hyps
  70   use ref.Ref
  71
  72   let lemma ind (n: int) requires { 0 <= n} ensures { p n }
  73     =
  74     let k = ref n in
  75     while !k >= 2 do
  76       invariant { 0 <= !k && (p !k -> p n) } variant { !k }
  77       k := !k - 2
  78     done
  79
  80   goal G: forall n: int. 0 <= n -> p n
  81
  82 end
  83
  84 (** {2 With an ascending while loop} *)
  85
  86 module LemmaFunction3
  87   use Hyps
  88   use ref.Ref
  89
  90   let lemma ind (n: int) requires { 0 <= n} ensures { p n }
  91     =
  92     let k = ref 0 in
  93     while !k <= n - 2 do
  94       invariant { 0 <= !k <= n && p !k && p (!k + 1) } variant { n - !k }
  95       k := !k + 2
  96     done
  97
  98   goal G: forall n: int. 0 <= n -> p n
  99
 100 end