Commit 7112d18b by Jean-Christophe Filliatre

### new example from unraveling a card trick'' (in progress)

parent db7b6bae
 (* Unraveling a Card Trick Tony Hoare and Natarajan Shankar Time for Verification Lecture Notes in Computer Science, 2010, Volume 6200/2010, 195-201, DOI: 10.1007/978-3-642-13754-9_10 http://www.springerlink.com/content/gn18673357154448/ *) module GilbreathCardTrick use import int.Int use import list.List use import list.Append use import list.Reverse use import module stack.Stack function m: int axiom m_positive: 0 < m function n: int axiom n_nonnegative: 0 <= n (* c is a riffle shuffle of a and b *) inductive shuffle (a b c: list 'a) = | Shuffle_nil_left: forall l: list 'a. shuffle l Nil l | Shuffle_nil_right: forall l: list 'a. shuffle Nil l l | Shuffle_cons_left: forall x: 'a, a b c: list 'a. shuffle a b c -> shuffle (Cons x a) b (Cons x c) | Shuffle_cons_right: forall x: 'a, a b c: list 'a. shuffle a b c -> shuffle a (Cons x b) (Cons x c) lemma shuffle_nil_nil_nil: shuffle Nil Nil (Nil: list 'a) lemma shuffle_length: forall a b c: list 'a. shuffle a b c -> L.length a + L.length b = L.length c let shuffle (a b: t int) = {} 'Init: let c = create () in while not (is_empty a && is_empty b) do invariant { exists a' b': list int. reverse (at a.elts 'Init) = reverse a.elts ++ a' /\ reverse (at b.elts 'Init) = reverse b.elts ++ b' /\ shuffle a' b' c.elts } variant { length a + length b } if not (is_empty a) && (is_empty b || any bool) then push (pop a) c else push (pop b) c done; c { a.elts = Nil /\ b.elts = Nil /\ shuffle (reverse (old a.elts)) (reverse (old b.elts)) result.elts } let card_trick (a: t int) = { length a = n*m } 'Init: (* cut a into c;d and reverse d in d_ *) let d_ = create () in let cut = any {} int { 0 <= result <= n*m } in for i = 1 to cut do invariant { length a = n*m-i+1 /\ length d_ = i-1 /\ at a.elts 'Init = reverse d_.elts ++ a.elts } push (pop a) d_ done; assert { at a.elts 'Init = reverse d_.elts ++ a.elts }; (* then suffle c (that is a) and d_ to get b *) 'Inter: shuffle a d_ { length result = n*m } end (* Local Variables: compile-command: "unset LANG; make -C ../.. examples/programs/unraveling_a_card_trick.gui" End: *)
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Definition unit := unit. Parameter qtmark : Type. Parameter at1: forall (a:Type), a -> qtmark -> a. Implicit Arguments at1. Parameter old: forall (a:Type), a -> a. Implicit Arguments old. Definition implb(x:bool) (y:bool): bool := match (x, y) with | (true, false) => false | (_, _) => true end. Inductive list (a:Type) := | Nil : list a | Cons : a -> (list a) -> list a. Set Contextual Implicit. Implicit Arguments Nil. Unset Contextual Implicit. Implicit Arguments Cons. Set Implicit Arguments. Fixpoint infix_plpl (a:Type)(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. Unset Implicit Arguments. Axiom Append_assoc : forall (a:Type), 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), forall (l:(list a)), ((infix_plpl l (Nil:(list a))) = l). Set Implicit Arguments. Fixpoint length (a:Type)(l:(list a)) {struct l}: Z := match l with | Nil => 0%Z | (Cons _ r) => (1%Z + (length r))%Z end. Unset Implicit Arguments. Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)), (0%Z <= (length l))%Z. Axiom Length_nil : forall (a:Type), forall (l:(list a)), ((length l) = 0%Z) <-> (l = (Nil:(list a))). Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)), ((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z). Set Implicit Arguments. Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop := match l with | Nil => False | (Cons y r) => (x = y) \/ (mem x r) end. Unset Implicit Arguments. Axiom mem_append : forall (a:Type), 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), forall (x:a) (l:(list a)), (mem x l) -> exists l1:(list a), exists l2:(list a), (l = (infix_plpl l1 (Cons x l2))). Set Implicit Arguments. Fixpoint reverse (a:Type)(l:(list a)) {struct l}: (list a) := match l with | Nil => (Nil:(list a)) | (Cons x r) => (infix_plpl (reverse r) (Cons x (Nil:(list a)))) end. Unset Implicit Arguments. Axiom reverse_append : forall (a:Type), forall (l1:(list a)) (l2:(list a)) (x:a), ((infix_plpl (reverse (Cons x l1)) l2) = (infix_plpl (reverse l1) (Cons x l2))). Axiom reverse_reverse : forall (a:Type), forall (l:(list a)), ((reverse (reverse l)) = l). Axiom Reverse_length : forall (a:Type), forall (l:(list a)), ((length (reverse l)) = (length l)). Inductive t (a:Type) := | mk_t : (list a) -> t a. Implicit Arguments mk_t. Definition elts (a:Type)(u:(t a)): (list a) := match u with | (mk_t elts1) => elts1 end. Implicit Arguments elts. Definition length1 (a:Type)(s:(t a)): Z := (length (elts s)). Implicit Arguments length1. Parameter m: Z. Axiom m_positive : (0%Z < m)%Z. Parameter n: Z. Axiom n_nonnegative : (0%Z <= n)%Z. Inductive shuffle{a:Type} : (list a) -> (list a) -> (list a) -> Prop := | Shuffle_nil_left : forall (l:(list a)), (shuffle l (Nil:(list a)) l) | Shuffle_nil_right : forall (l:(list a)), (shuffle (Nil:(list a)) l l) | Shuffle_cons_left : forall (x:a) (a1:(list a)) (b:(list a)) (c:(list a)), (shuffle a1 b c) -> (shuffle (Cons x a1) b (Cons x c)) | Shuffle_cons_right : forall (x:a) (a1:(list a)) (b:(list a)) (c:(list a)), (shuffle a1 b c) -> (shuffle a1 (Cons x b) (Cons x c)). Implicit Arguments shuffle. (* YOU MAY EDIT THE CONTEXT BELOW *) (* DO NOT EDIT BELOW *) Theorem WP_parameter_card_trick : forall (a:(list Z)), ((length a) = (n * m)%Z) -> forall (result:(list Z)), (result = (Nil:(list Z))) -> forall (result1:Z), ((0%Z <= result1)%Z /\ (result1 <= (n * m)%Z)%Z) -> ((1%Z <= result1)%Z -> forall (d_:(list Z)), forall (a1:(list Z)), (((length a1) = (((n * m)%Z - (result1 + 1%Z)%Z)%Z + 1%Z)%Z) /\ (((length d_) = ((result1 + 1%Z)%Z - 1%Z)%Z) /\ (a = (infix_plpl (reverse d_) a1)))) -> ((a = (infix_plpl (reverse d_) a1)) -> forall (result2:(list Z)), (result2 = (Nil:(list Z))) -> exists aqt:(list Z), exists dqt:(list Z), (a1 = (infix_plpl (reverse aqt) a1)) /\ ((d_ = (infix_plpl (reverse dqt) d_)) /\ (shuffle aqt dqt result2)))). (* YOU MAY EDIT THE PROOF BELOW *) intuition. exists Nil; exists Nil; intuition. subst result2; apply Shuffle_nil_left. Qed. (* DO NOT EDIT BELOW *)
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Definition unit := unit. Parameter qtmark : Type. Parameter at1: forall (a:Type), a -> qtmark -> a. Implicit Arguments at1. Parameter old: forall (a:Type), a -> a. Implicit Arguments old. Definition implb(x:bool) (y:bool): bool := match (x, y) with | (true, false) => false | (_, _) => true end. Inductive list (a:Type) := | Nil : list a | Cons : a -> (list a) -> list a. Set Contextual Implicit. Implicit Arguments Nil. Unset Contextual Implicit. Implicit Arguments Cons. Set Implicit Arguments. Fixpoint infix_plpl (a:Type)(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. Unset Implicit Arguments. Axiom Append_assoc : forall (a:Type), 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), forall (l:(list a)), ((infix_plpl l (Nil:(list a))) = l). Set Implicit Arguments. Fixpoint length (a:Type)(l:(list a)) {struct l}: Z := match l with | Nil => 0%Z | (Cons _ r) => (1%Z + (length r))%Z end. Unset Implicit Arguments. Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)), (0%Z <= (length l))%Z. Axiom Length_nil : forall (a:Type), forall (l:(list a)), ((length l) = 0%Z) <-> (l = (Nil:(list a))). Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)), ((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z). Set Implicit Arguments. Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop := match l with | Nil => False | (Cons y r) => (x = y) \/ (mem x r) end. Unset Implicit Arguments. Axiom mem_append : forall (a:Type), 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), forall (x:a) (l:(list a)), (mem x l) -> exists l1:(list a), exists l2:(list a), (l = (infix_plpl l1 (Cons x l2))). Set Implicit Arguments. Fixpoint reverse (a:Type)(l:(list a)) {struct l}: (list a) := match l with | Nil => (Nil:(list a)) | (Cons x r) => (infix_plpl (reverse r) (Cons x (Nil:(list a)))) end. Unset Implicit Arguments. Axiom reverse_append : forall (a:Type), forall (l1:(list a)) (l2:(list a)) (x:a), ((infix_plpl (reverse (Cons x l1)) l2) = (infix_plpl (reverse l1) (Cons x l2))). Axiom reverse_reverse : forall (a:Type), forall (l:(list a)), ((reverse (reverse l)) = l). Axiom Reverse_length : forall (a:Type), forall (l:(list a)), ((length (reverse l)) = (length l)). Inductive t (a:Type) := | mk_t : (list a) -> t a. Implicit Arguments mk_t. Definition elts (a:Type)(u:(t a)): (list a) := match u with | (mk_t elts1) => elts1 end. Implicit Arguments elts. Definition length1 (a:Type)(s:(t a)): Z := (length (elts s)). Implicit Arguments length1. Parameter m: Z. Axiom m_positive : (0%Z < m)%Z. Parameter n: Z. Axiom n_nonnegative : (0%Z <= n)%Z. Inductive shuffle{a:Type} : (list a) -> (list a) -> (list a) -> Prop := | Shuffle_nil_left : forall (l:(list a)), (shuffle l (Nil:(list a)) l) | Shuffle_nil_right : forall (l:(list a)), (shuffle (Nil:(list a)) l l) | Shuffle_cons_left : forall (x:a) (a1:(list a)) (b:(list a)) (c:(list a)), (shuffle a1 b c) -> (shuffle (Cons x a1) b (Cons x c)) | Shuffle_cons_right : forall (x:a) (a1:(list a)) (b:(list a)) (c:(list a)), (shuffle a1 b c) -> (shuffle a1 (Cons x b) (Cons x c)). Implicit Arguments shuffle. Axiom shuffle_nil_nil_nil : forall (a:Type), (shuffle (Nil:(list a)) (Nil:(list a)) (Nil:(list a))). Axiom shuffle_length : forall (a:Type), forall (a1:(list a)) (b:(list a)) (c:(list a)), (shuffle a1 b c) -> (((length a1) + (length b))%Z = (length c)). (* YOU MAY EDIT THE CONTEXT BELOW *) (* DO NOT EDIT BELOW *) Theorem WP_parameter_shuffle : forall (b:(list Z)), forall (a:(list Z)), forall (result:(list Z)), (result = (Nil:(list Z))) -> forall (c:(list Z)), forall (b1:(list Z)), forall (a1:(list Z)), (exists aqt:(list Z), (exists bqt:(list Z), ((reverse a) = (infix_plpl (reverse a1) aqt)) /\ (((reverse b) = (infix_plpl (reverse b1) bqt)) /\ (shuffle aqt bqt c)))) -> forall (result1:bool), ((result1 = true) <-> (a1 = (Nil:(list Z)))) -> ((result1 = true) -> forall (result2:bool), ((result2 = true) <-> (b1 = (Nil:(list Z)))) -> ((~ (result2 = true)) -> forall (result3:bool), ((result3 = true) <-> (a1 = (Nil:(list Z)))) -> ((result3 = true) -> forall (b2:(list Z)), forall (result4:Z), match b1 with | Nil => False | (Cons x t1) => (result4 = x) /\ (b2 = t1) end -> forall (c1:(list Z)), (c1 = (Cons result4 c)) -> exists aqt:(list Z), exists bqt:(list Z), ((reverse a) = (infix_plpl (reverse a1) aqt)) /\ (((reverse b) = (infix_plpl (reverse b2) bqt)) /\ (shuffle aqt bqt c1))))). (* YOU MAY EDIT THE PROOF BELOW *) intuition. destruct H0 as (a', (b', (h1, (h2, h3)))). subst. exists a'; exists (Cons result4 b'). destruct b1. inversion H9. intuition (subst; clear H5 H6 H10 H7 H4 H3 result2). rewrite h2. rewrite reverse_append. auto. apply Shuffle_cons_right; auto. Qed. (* DO NOT EDIT BELOW *)
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Definition unit := unit. Parameter qtmark : Type. Parameter at1: forall (a:Type), a -> qtmark -> a. Implicit Arguments at1. Parameter old: forall (a:Type), a -> a. Implicit Arguments old. Definition implb(x:bool) (y:bool): bool := match (x, y) with | (true, false) => false | (_, _) => true end. Inductive list (a:Type) := | Nil : list a | Cons : a -> (list a) -> list a. Set Contextual Implicit. Implicit Arguments Nil. Unset Contextual Implicit. Implicit Arguments Cons. Set Implicit Arguments. Fixpoint infix_plpl (a:Type)(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. Unset Implicit Arguments. Axiom Append_assoc : forall (a:Type), 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), forall (l:(list a)), ((infix_plpl l (Nil:(list a))) = l). Set Implicit Arguments. Fixpoint length (a:Type)(l:(list a)) {struct l}: Z := match l with | Nil => 0%Z | (Cons _ r) => (1%Z + (length r))%Z end. Unset Implicit Arguments. Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)), (0%Z <= (length l))%Z. Axiom Length_nil : forall (a:Type), forall (l:(list a)), ((length l) = 0%Z) <-> (l = (Nil:(list a))). Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)), ((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z). Set Implicit Arguments. Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop := match l with | Nil => False | (Cons y r) => (x = y) \/ (mem x r) end. Unset Implicit Arguments. Axiom mem_append : forall (a:Type), 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), forall (x:a) (l:(list a)), (mem x l) -> exists l1:(list a), exists l2:(list a), (l = (infix_plpl l1 (Cons x l2))). Set Implicit Arguments. Fixpoint reverse (a:Type)(l:(list a)) {struct l}: (list a) := match l with | Nil => (Nil:(list a)) | (Cons x r) => (infix_plpl (reverse r) (Cons x (Nil:(list a)))) end. Unset Implicit Arguments. Axiom reverse_append : forall (a:Type), forall (l1:(list a)) (l2:(list a)) (x:a), ((infix_plpl (reverse (Cons x l1)) l2) = (infix_plpl (reverse l1) (Cons x l2))). Axiom reverse_reverse : forall (a:Type), forall (l:(list a)), ((reverse (reverse l)) = l). Axiom Reverse_length : forall (a:Type), forall (l:(list a)), ((length (reverse l)) = (length l)). Inductive t (a:Type) := | mk_t : (list a) -> t a. Implicit Arguments mk_t. Definition elts (a:Type)(u:(t a)): (list a) := match u with | (mk_t elts1) => elts1 end. Implicit Arguments elts. Definition length1 (a:Type)(s:(t a)): Z := (length (elts s)). Implicit Arguments length1. Parameter m: Z. Axiom m_positive : (0%Z < m)%Z. Parameter n: Z. Axiom n_nonnegative : (0%Z <= n)%Z. Inductive shuffle{a:Type} : (list a) -> (list a) -> (list a) -> Prop := | Shuffle_nil_left : forall (l:(list a)), (shuffle l (Nil:(list a)) l) | Shuffle_nil_right : forall (l:(list a)), (shuffle (Nil:(list a)) l l) | Shuffle_cons_left : forall (x:a) (a1:(list a)) (b:(list a)) (c:(list a)), (shuffle a1 b c) -> (shuffle (Cons x a1) b (Cons x c)) | Shuffle_cons_right : forall (x:a) (a1:(list a)) (b:(list a)) (c:(list a)), (shuffle a1 b c) -> (shuffle a1 (Cons x b) (Cons x c)). Implicit Arguments shuffle. Axiom shuffle_nil_nil_nil : forall (a:Type), (shuffle (Nil:(list a)) (Nil:(list a)) (Nil:(list a))). Axiom shuffle_length : forall (a:Type), forall (a1:(list a)) (b:(list a)) (c:(list a)), (shuffle a1 b c) -> (((length a1) + (length b))%Z = (length c)). (* YOU MAY EDIT THE CONTEXT BELOW *) (* DO NOT EDIT BELOW *) Theorem WP_parameter_shuffle : forall (b:(list Z)), forall (a:(list Z)), forall (result:(list Z)), (result = (Nil:(list Z))) -> forall (c:(list Z)), forall (b1:(list Z)), forall (a1:(list Z)), (exists aqt:(list Z), (exists bqt:(list Z), ((reverse a) = (infix_plpl (reverse a1) aqt)) /\ (((reverse b) = (infix_plpl (reverse b1) bqt)) /\ (shuffle aqt bqt c)))) -> forall (result1:bool), ((result1 = true) <-> (a1 = (Nil:(list Z)))) -> ((~ (result1 = true)) -> forall (result2:bool), ((result2 = true) <-> (a1 = (Nil:(list Z)))) -> ((~ (result2 = true)) -> forall (result3:bool), ((result3 = true) <-> (b1 = (Nil:(list Z)))) -> forall (result4:bool), ((result3 = true) \/ (result4 = true)) -> forall (a2:(list Z)), forall (result5:Z), match a1 with | Nil => False | (Cons x t1) => (result5 = x) /\ (a2 = t1) end -> forall (c1:(list Z)), (c1 = (Cons result5 c)) -> exists aqt:(list Z), exists bqt:(list Z), ((reverse a) = (infix_plpl (reverse a2) aqt)) /\ (((reverse b) = (infix_plpl (reverse b1) bqt)) /\ (shuffle aqt bqt c1)))). (* YOU MAY EDIT THE PROOF BELOW *) intros. clear H6. intuition. destruct H0 as (a', (b', (h1, (h2, h3)))). subst. exists (Cons result5 a'); exists b'. destruct a1. inversion H7. intuition (subst; clear H2 H4 H6 H9 H1 H3 H11 H10 result2 result1 result3 result4). rewrite h1. rewrite reverse_append. auto. apply Shuffle_cons_left; auto. Qed. (* DO NOT EDIT BELOW *)
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Definition unit := unit. Parameter qtmark : Type. Parameter at1: forall (a:Type), a -> qtmark -> a. Implicit Arguments at1. Parameter old: forall (a:Type), a -> a. Implicit Arguments old. Definition implb(x:bool) (y:bool): bool := match (x, y) with | (true, false) => false | (_, _) => true end. Inductive list (a:Type) := | Nil : list a | Cons : a -> (list a) -> list a. Set Contextual Implicit. Implicit Arguments Nil. Unset Contextual Implicit. Implicit Arguments Cons. Set Implicit Arguments. Fixpoint infix_plpl (a:Type)(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.