Commit 72e24dba by Jean-Christophe Filliatre

### new example: random access lists

`features polymorphic recursion, both in the logic and in programs`
parent ac0cd54a
 (** Random Access Lists. The code below uses polymorphic recursion (both in the logic and in the programs). BUGS: - induction_ty_lex has no effect on a goal involving polymorphic recursion - a lemma function is not allowed to perform polymorphic recursion? *) module RandomAccessList use import int.Int use import int.ComputerDivision use import list.List use import list.Length use import list.Nth use import option.Option type ral 'a = | Empty | Zero (ral ('a, 'a)) | One 'a (ral ('a, 'a)) function flatten (l: list ('a , 'a)) : list 'a = match l with | Nil -> Nil | Cons (x, y) l1 -> Cons x (Cons y (flatten l1)) end lemma length_flatten: forall l: list ('a, 'a). length (flatten l) = 2 * length l function elements (l: ral 'a) : list 'a = match l with | Empty -> Nil | Zero l1 -> flatten (elements l1) | One x l1 -> Cons x (flatten (elements l1)) end let rec size (l: ral 'a) : int variant { l } ensures { result = length (elements l) } = match l with | Empty -> 0 | Zero l1 -> 2 * size l1 | One _ l1 -> 1 + 2 * size l1 end let rec add (x: 'a) (l: ral 'a) : ral 'a variant { l } ensures { elements result = Cons x (elements l) } = match l with | Empty -> One x Empty | Zero l1 -> One x l1 | One y l1 -> Zero (add (x, y) l1) end let rec lemma nth_flatten (i: int) (l: list ('a, 'a)) requires { 0 <= i < length l } variant { l } ensures { match nth i l with | None -> false | Some (x0, x1) -> Some x0 = nth (2 * i) (flatten l) /\ Some x1 = nth (2 * i + 1) (flatten l) end } = match l with | Nil -> () | Cons _ r -> if i > 0 then nth_flatten (i-1) r end let rec get (i: int) (l: ral 'a) : 'a requires { 0 <= i < length (elements l) } variant { i, l } ensures { nth i (elements l) = Some result } = match l with | Empty -> absurd | One x l1 -> if i = 0 then x else get (i-1) (Zero l1) | Zero l1 -> let (x0, x1) = get (div i 2) l1 in if mod i 2 = 0 then x0 else x1 end end
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require BuiltIn. Require int.Int. Require int.Abs. Require int.ComputerDivision. Require list.List. Require list.Length. Require list.Nth. Require option.Option. (* Why3 assumption *) Definition unit := unit. Axiom qtmark : Type. Parameter qtmark_WhyType : WhyType qtmark. Existing Instance qtmark_WhyType. (* Why3 assumption *) Inductive ral (a:Type) := | Empty : ral a | Zero : (ral (a* a)%type) -> ral a | One : a -> (ral (a* a)%type) -> ral a. Axiom ral_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ral a). Existing Instance ral_WhyType. Implicit Arguments Empty [[a]]. Implicit Arguments Zero [[a]]. Implicit Arguments One [[a]]. (* Why3 assumption *) Fixpoint flatten {a:Type} {a_WT:WhyType a} (l:(list (a* a)%type)) {struct l}: (list a) := match l with | Init.Datatypes.nil => Init.Datatypes.nil | (Init.Datatypes.cons (x, y) l1) => (Init.Datatypes.cons x (Init.Datatypes.cons y (flatten l1))) end. (* Why3 goal *) Theorem length_flatten : forall {a:Type} {a_WT:WhyType a}, forall (l:(list (a* a)%type)), ((list.Length.length (flatten l)) = (2%Z * (list.Length.length l))%Z). intros a a_WT l. induction l. auto. simpl (flatten (a0::l)). destruct a0. replace (Length.length ((a0,a1)::l)) with (1 + (Length.length l))%Z by auto. unfold Length.length at 1; fold Length.length. rewrite IHl. ring. Qed.