Commit d41cca42 by Jean-Christophe Filliâtre

### programs: more theories, more examples

parent 3f2a8a9b
 ... ... @@ -13,21 +13,22 @@ let rec f91 (n:int) : int variant { 101-n } = (* non-recursive version *) { logic f int : int logic f (x:int) : int = if x >= 101 then x-10 else 91 axiom F_def1 : forall x:int. x >= 101 -> f(x) = x-10 axiom F_def2 : forall x:int. x <= 101 -> f(x) = 91 (* iter_f(n,x) = f^n(x) *) logic iter_f (n x:int) : int = if n = 0 then x else iter_f (n-1) (f x) logic iter_f int int : int (* iter_f(n,x) = f^n(x) *) axiom Iter_f_def1 : forall x:int. iter_f 0 x = x axiom Iter_f_def2 : forall n x:int. n > 0 -> iter_f n x = iter_f (n-1) (f x) inductive lex (int,int) (int,int) = | Lex_1: forall x1 y1 x2 y2 : int. lt_nat x1 x2 -> lex (x1,y1) (x2,y2) | Lex_2: forall x y1 y2 : int. lt_nat y1 y2 -> lex (x,y1) (x,y2) (* clone import relations.Lex with type t1 = int, type t2 = int, logic r1 = lt_nat, logic r2 = lt_int *) inductive lex (int,int) (int,int) = | Lex_1: forall x1 y1 x2 y2 : int. lt_nat x1 x2 -> lex (x1,y1) (x2,y2) | Lex_2: forall x y1 y2 : int. lt_nat y1 y2 -> lex (x,y1) (x,y2) } let f91_nonrec (n:ref int) (x:ref int) = ... ...
 { use import int.EuclideanDivision use import int.Power logic sum_digits (n:int) : int = if n = 0 then 0 else sum_digits (div n 10) + mod n 10 logic p (n:int) = sum_digits(n) = sum_digits(137 * n) clone int.NumOf as P with logic p = p type int2 = (int,int) logic q (d:int2) (n:int) = let (a,b) = d in sum_digits(n) = sum_digits(137 * n + a) = b clone int.NumOfDep as Q with type dep = int2, logic p = q goal Test : forall n:int. 0 <= n < power 10 0 -> n = 0 } { (* use import int.ComputerDivision *) } let rec sd n = { n >= 0 } if n = 0 then 0 else sd (div n 10) + mod n 10 { result = sum_digits n } (* f(m,a,b) = the number of 0 <= n < 10^m such that digitsum(n) = digitsum(137n+a)+b. *) let rec f m a b = { 0 <= m } if m = 0 then begin (* only n = 0 is possible *) if sum_digits a + b = 0 then 1 else 0 end else begin let sum = ref 0 in let c = ref 0 in while !c <= 9 do (* n = 10n' + c *) invariant { 0 <= !c <= 10 } variant { !c } let x = 137 * !c + a in let a' = div x 10 in let c' = mod x 10 in sum := !sum + f (m-1) a' (c' + b - !c); c := !c + 1 done; !sum end { result = Q.num_of (a,b) 0 (power 10 m) } (* Local Variables: compile-command: "unset LANG; make -C ../.. examples/programs/talk290" End: *)
 ... ... @@ -85,3 +85,57 @@ theory ComputerDivision end theory Power use import Int logic power (x n : int) : int = if n = 0 then 1 else x * power x (n-1) end theory NumOf use import Int logic p int (* number of n st a <= n < b and p(n) *) logic num_of (a b : int) : int axiom Num_of_empty : forall a b : int. b <= a -> num_of a b = 0 axiom Num_of_zero : forall a b : int. a < b -> not p a -> num_of a b = num_of (a+1) b axiom Num_of_one : forall a b : int. a < b -> p a -> num_of a b = 1 + num_of (a+1) b axiom Num_of_append : forall a b c : int. a < b < c -> num_of a c = num_of a b + num_of b c end theory NumOfDep type dep use import Int logic p dep int (* number of n st a <= n < b and p(d,n) *) logic num_of dep (a b : int) : int axiom Num_of_empty : forall d : dep, a b : int. b <= a -> num_of d a b = 0 axiom Num_of_zero : forall d : dep, a b : int. a < b -> not p d a -> num_of d a b = num_of d (a+1) b axiom Num_of_one : forall d : dep, a b : int. a < b -> p d a -> num_of d a b = 1 + num_of d (a+1) b axiom Num_of_append : forall d : dep, a b c : int. a < b < c -> num_of d a c = num_of d a b + num_of d b c end
 ... ... @@ -162,6 +162,24 @@ theory TotalOrder end *) (* theory Lex type t1 type t2 logic r1 t1 t1 logic r2 t2 t2 inductive lex (t1, t2) (t1, t2) = | Lex_1: forall (x1 x2 : t1) (y1 y2 : t2). r1 x1 x2 -> lex (x1,y1) (x2,y2) | Lex_2: forall (x : t1) (y1 y2 : t2). r2 y1 y2 -> lex (x,y1) (x,y2) end *) (* theory MinMax ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment