Initial commit

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 import 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 import Nat
+  (* use import Add *)
+  (* use import 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 import Nat
+ use import 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 *)
+ 
+ 
+ (* 
+    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) = (* 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. ... -> sub n m < n
+   
+ *)
+end	
\ No newline at end of file