Commit 236f9c53 by Jean-Christophe Filliâtre

there and back again: second puzzle

parent 7bb59738
 (* Puzzle from Olivier Danvy's ``There and back again'' (* Two puzzles from Danvy and Goldberg's ``There and back again'' http://www.brics.dk/RS/02/12/BRICS-RS-02-12.pdf‎ *) Given two lists of the same length, [x1;x2;...;xn] and [y1;y2;...;yn], build the list of pairs [(x1,yn); (x2,yn-1); ...; (xn,y1)] in linear time using only n recursive calls. (* Computing a symbolic convolution: Given two lists [x1 , x2 , ..., xn−1 , xn ] and [y1 , y2 , ..., yn−1 , yn ], where n is not known in advance, write a function that constructs [(x1 , yn ), (x2 , yn−1 ), ..., (xn−1 , y2 ), (xn , y1 )] in n recursive calls and with no auxiliary list. *) module ThereAndBackAgain module Convolution use import int.Int use import list.List ... ... @@ -16,7 +20,7 @@ module ThereAndBackAgain use import list.Reverse use import list.Combine let rec product (x y: list 'a) : (list ('a, 'a), list 'a) let rec convolution_rec (x y: list 'a) : (list ('a, 'a), list 'a) variant { x } requires { length x <= length y } ensures { let (r, ys) = result in exists y0: list 'a. ... ... @@ -26,14 +30,64 @@ module ThereAndBackAgain | Nil -> (Nil, y) | Cons x0 xs -> match product xs y with match convolution_rec xs y with | r, Cons y0 ys -> (Cons (x0, y0) r, ys) | _ -> absurd end end let puzzle (x y: list 'a) : list ('a, 'a) let convolution (x y: list 'a) : list ('a, 'a) requires { length x = length y } ensures { result = combine x (reverse y) } = let r, _ = product x y in r = let r, _ = convolution_rec x y in r end (* Detecting a palindrome: Given a list of length n, where n is not known in advance, determine whether this list is a palindrome in ceil(n/2) recursive calls and with no auxiliary list. *) module Palindrome use import int.Int use import list.List use import list.Length use import list.Append use import list.Nth use import list.NthLength use import list.NthLengthAppend predicate pal (x: list 'a) (n: int) = forall i: int. 0 <= i < n -> nth i x = nth (n - 1 - i) x exception Exit let rec palindrome_rec (x y: list 'a) : list 'a requires { length x >= length y } variant { x } ensures { exists x0: list 'a. length x0 = length y && x = x0 ++ result } ensures { pal x (length y) } raises { Exit -> exists i: int. 0 <= i < length y && nth i x <> nth (length y - 1 - i) x } = match x, y with | _, Nil -> x | Cons _ xs, Cons _ Nil -> xs | Cons x0 xs, Cons _ (Cons _ ys) -> match palindrome_rec xs ys with | Cons x1 xs -> assert { nth (length y - 1) x = Some x1 }; if x0 = x1 then xs else raise Exit | Nil -> absurd end | _ -> absurd end let palindrome (x: list 'a) : bool ensures { result=True <-> pal x (length x) } = try let _ = palindrome_rec x x in True with Exit -> False end end
 (* This file is generated by Why3's Coq 8.4 driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require BuiltIn. Require int.Int. Require list.List. Require list.Length. Require list.Nth. Require option.Option. Require list.NthLength. (* Why3 assumption *) Definition unit := unit. (* Why3 assumption *) Fixpoint infix_plpl {a:Type} {a_WT:WhyType a} (l1:list a) (l2:list a) {struct l1}: list a := match l1 with | nil => l2 | (cons x1 r1) => (cons x1 (infix_plpl r1 l2)) end. Axiom Append_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:list a) (l2:list a) (l3:list a), ((infix_plpl l1 (infix_plpl l2 l3)) = (infix_plpl (infix_plpl l1 l2) l3)). Axiom Append_l_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:list a), ((infix_plpl l nil) = l). Axiom Append_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:list a) (l2:list a), ((list.Length.length (infix_plpl l1 l2)) = ((list.Length.length l1) + (list.Length.length l2))%Z). (* Why3 assumption *) Fixpoint mem {a:Type} {a_WT:WhyType a} (x:a) (l:list a) {struct l}: Prop := match l with | nil => False | (cons y r) => (x = y) \/ (mem x r) end. Axiom mem_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:list a) (l2:list a), (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x l2)). Axiom mem_decomp : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:list a), (mem x l) -> exists l1:list a, exists l2:list a, (l = (infix_plpl l1 (cons x l2))). Axiom nth_append_1 : forall {a:Type} {a_WT:WhyType a}, forall (l1:list a) (l2:list a) (i:Z), (i < (list.Length.length l1))%Z -> ((list.Nth.nth i (infix_plpl l1 l2)) = (list.Nth.nth i l1)). Axiom nth_append_2 : forall {a:Type} {a_WT:WhyType a}, forall (l1:list a) (l2:list a) (i:Z), ((list.Length.length l1) <= i)%Z -> ((list.Nth.nth i (infix_plpl l1 l2)) = (list.Nth.nth (i - (list.Length.length l1))%Z l2)). (* Why3 assumption *) Definition pal {a:Type} {a_WT:WhyType a} (x:list a) (n:Z): Prop := forall (i:Z), ((0%Z <= i)%Z /\ (i < n)%Z) -> ((list.Nth.nth i x) = (list.Nth.nth ((n - 1%Z)%Z - i)%Z x)). (* Why3 goal *) Theorem WP_parameter_palindrome_rec : forall {a:Type} {a_WT:WhyType a}, forall (x:list a) (y:list a), ((list.Length.length y) <= (list.Length.length x))%Z -> match y with | (cons x1 x2) => match x2 with | (cons x3 x4) => match x with | (cons x5 x6) => ((list.Length.length x4) <= (list.Length.length x6))%Z -> ((exists i:Z, ((0%Z <= i)%Z /\ (i < (list.Length.length x4))%Z) /\ ~ ((list.Nth.nth i x6) = (list.Nth.nth (((list.Length.length x4) - 1%Z)%Z - i)%Z x6))) -> exists i:Z, ((0%Z <= i)%Z /\ (i < (list.Length.length y))%Z) /\ ~ ((list.Nth.nth i x) = (list.Nth.nth (((list.Length.length y) - 1%Z)%Z - i)%Z x))) | _ => True end | nil => True end | nil => True end. intros a a_WT x y h1. destruct y; auto. destruct y; auto. destruct x; auto. intros hl (i, (hi1, hi2)). exists (i+1)%Z; intuition. unfold Length.length. fold Length.length. omega. unfold Length.length in *. fold Length.length in *. assert (Nth.nth (i+1) (a2 :: x) = Nth.nth i x). unfold Nth.nth; fold Nth.nth. generalize (Zeq_bool_eq (i+1) 0). destruct (Zeq_bool (i+1) 0). intuition. elimtype False. omega. intuition. replace (i+1-1)%Z with i by omega. auto. replace (1 + (1 + Length.length y) - 1 - (i + 1))%Z with (1 + Length.length y - 1 - i)%Z in H1 by omega. assert (Nth.nth (1 + Length.length y - 1 - i) (a2 :: x) = Nth.nth (Length.length y - 1 - i) x). unfold Nth.nth; fold Nth.nth. generalize (Zeq_bool_eq (1 + Length.length y - 1 - i) 0). destruct (Zeq_bool (1 + Length.length y - 1 - i) 0). intuition; elimtype False; omega. intuition. replace (1 + Length.length y - 1 - i - 1)%Z with (Length.length y - 1 - i)%Z by omega; auto. congruence. Qed.
This diff is collapsed.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!