peano_nat.mlw

module Nat

  type nat = O | S nat
  
  function add (n1 n2 : nat) : nat =
    match n1 with
    | O   -> n2
    | S n -> S (add n n2)
    end 

  function (+) (a b : nat) : nat = add a b
  
  use int.Int
  goal g:
    forall x. x = 1 -> x > 0
end

module TestAdd

  use Nat

  goal g_0_0: (* 0 + 0 = 0 *)
    O + O = O
  (* solved by "compute_in_goal" *)

  goal g_0_1: (* 0 + 1 = 1 *)
    O + S O = S O
  (* solved by "compute_in_goal" *)

  goal g_2_1: (* 2 + 1 = 3 *)
    S (S O) + S O = S (S (S O)) 
  (* solved by "compute_in_goal" *)
  
end

module Inconsistency

  lemma introduce: true -> false   (* <-- introduces inconsistency *)
  
  lemma exposed:   true -> false   (* <-- exposed to inconsistency *)

  (* 
    incosisitency applies in this scope,
    and all scopes the "use" this module (transitively)
  *)  
end


module Add

  use Nat
  
  goal plus_ol: 
    forall n. O + n = n
  (* solved by "compute_in_goal" *)
    
  goal plus_o_right:
    forall n. n + O = n
  (* solved by numerous transformations *)
     
  
  goal plus_o_right_altergo:
    forall n. n + O = n
  (* solved by two simple transofrmations and SMT solver
     "inline_goal"
     "induction_ty_lex"
     "altergo" 
  *)
  
  (* we want to prove commutativity *)
  
  (* facilitates plus_comm *)
  lemma plus_o_right_lemma:
    forall n. n + O = n
  (* solved by two simple transofrmations and SMT solver
     "inline_goal"
     "induction_ty_lex"
     "altergo"
  *) 
  
  (* not required to solve plus_comm *)
  (* but might be useful to other proofs *)
  lemma plus_Snm_nSm : forall n m:nat. (S n) + m = n + (S m) 
  (* solved by two simple transofrmations and SMT solver
     "inline_goal"
     "induction_ty_lex"
     "altergo" 
  *)
  
  (* facilitates plus_comm *)
  lemma plus_S: forall n m:nat. S (n + m) = n + (S m) 
  (* solved by two simple transofrmations and SMT solver
     "inline_goal"
     "induction_ty_lex"
     "altergo" 
  *)
  
  (* our final goal *)
  goal plus_comm:
    forall n m. n + m = m + n
  (* solved by two simple transofrmations and SMT solver
     "inline_goal"
     "induction_ty_lex"
     "altergo" 
  *)
end

module Compare

  use Nat
  use Add
  (* use Inconsistency *)
 
  inductive le nat nat = 
  | Le_n : forall n:nat. le n n
  | Le_S : forall n m:nat. le n m -> le n (S m)

  predicate (<=) (x y:nat) = le x y
  predicate (<)  (x y:nat) = (S x) <= y
  
  
  function f (x : nat) : nat = x + (S O)
 
  goal f_proof:
   forall x. x < f x
  
  function g (x y: nat) : nat = x + y 

  goal g_proof:
    forall x y [@induction]. x <= g x y
end


module Sub
 use Nat
 use Compare
 
 function sub (n m:nat) : nat =
 match n, m with
 | S k, S l -> sub k l
 | _, _ -> n
 end
 
 (* Assignment 3a *) 
 
 inductive sub_pr nat nat nat = (* your code here *)
 | sub_pr_1 : forall n m r:nat. sub_pr n m r -> sub_pr (S n) (S m) r
 | sub_pr_2 : forall n:nat. sub_pr n O n
 | sub_pr_3 : forall m:nat. sub_pr O m O
 
 
 (* 
    show the correspondence in between the
    inductive predicate sub_pr and the
    function sub
 *)
 
 
 lemma sub_equivalence:
  forall n m l. l = sub n m <-> sub_pr n m l
 
 (* Assignment 3b *)   
 lemma sub_le_nm:
    forall n m. sub n m <= n
 
 (* Assignment 3c *)   
 predicate (>=) (x y:nat) = le y x (* your code here *)
  
 lemma sub_ge_nm:
    forall n m. n >= sub n m
    
 (* Assignment 3d *)   
 predicate (<) (x y:nat) = le (S x) y 
 
 lemma sub_lt_nm:
    forall n m. ((n <> O) /\ (m <> O)) -> sub n m < n
   
 
end