Gilbreath's card trick: program part completed

examples/programs/unraveling_a_card_trick.mlw

@@ -15,6 +15,7 @@ theory GilbreathCardTrick
   use export list.Length
   use export list.Append
   use export list.Reverse
+  use import list.Nth
 
   function m: int
   axiom m_positive: 0 < m
@@ -37,9 +38,29 @@ theory GilbreathCardTrick
 
   lemma shuffle_nil_nil_nil: shuffle Nil Nil (Nil: list 'a)
 
+  lemma shuffle_sym:
+     forall a b c: list 'a. shuffle a b c -> shuffle b a c
+
   lemma shuffle_length:
     forall a b c: list 'a. shuffle a b c -> length a + length b = length c
 
+  (* the list l is composed of n blocks, each being 0,1,...,m-1 *)
+  predicate suit_ordered (l: list int) =
+    forall i j: int. 0 <= i < n -> 0 <= j < m -> nth (i * m + j) l = Some j
+
+  (* the list l is a sequence of n blocks,
+     each being a permutation of 0,1,...,m-1 *)
+  predicate suit_sorted (l: list int) =
+    (forall i v: int. nth i l = Some v -> 0 <= v < m) /\
+    (forall i j1 j2: int. 0 <= i < n -> 0 <= j1 < m -> 0 <= j2 < m ->
+     nth (i * m + j1) l <> nth (i * m + j2) l)
+
+  (* TODO: prove it! *)
+  axiom gilbreath_card_trick:
+    forall a: list int. length a = n * m -> suit_ordered a ->
+    forall c d: list int. a = c ++ d ->
+    forall b: list int. shuffle c (reverse d) b -> suit_sorted b
+
 end
 
 (* a program implementing the card trick using stacks *)
@@ -70,7 +91,7 @@ module GilbreathCardTrick
       shuffle (reverse (old a.elts)) (reverse (old b.elts)) result.elts }
 
   let card_trick (a: t int) =
-    { length a = n*m }
+    { length a = n*m /\ suit_ordered a.elts }
     'Init:
     (* cut a into c;d and reverse d in d_ *)
     let d_ = create () in
@@ -82,9 +103,8 @@ module GilbreathCardTrick
     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 }
+    { length result = n*m && suit_sorted result.elts }
 
 end
 

examples/programs/unraveling_a_card_trick/unraveling_a_card_trick_GilbreathCardTrick_shuffle_sym_1.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+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 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))).
+
+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).
+
+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 option (a:Type) :=
+  | None : option a
+  | Some : a -> option a.
+Set Contextual Implicit.
+Implicit Arguments None.
+Unset Contextual Implicit.
+Implicit Arguments Some.
+
+Parameter nth: forall (a:Type), Z -> (list a) -> (option a).
+
+Implicit Arguments nth.
+
+Axiom nth_def : forall (a:Type), forall (n:Z) (l:(list a)),
+  match l with
+  | Nil => ((nth n l) = (None:(option a)))
+  | (Cons x r) => ((n = 0%Z) -> ((nth n l) = (Some x))) /\ ((~ (n = 0%Z)) ->
+      ((nth n l) = (nth (n - 1%Z)%Z r)))
+  end.
+
+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))).
+
+(* YOU MAY EDIT THE CONTEXT BELOW *)
+Hint Constructors shuffle.
+(* DO NOT EDIT BELOW *)
+
+Theorem shuffle_sym : forall (a:Type), forall (a1:(list a)) (b:(list a))
+  (c:(list a)), (shuffle a1 b c) -> (shuffle b a1 c).
+(* YOU MAY EDIT THE PROOF BELOW *)
+induction 1; intuition.
+Qed.
+(* DO NOT EDIT BELOW *)
+
+