Commit b6149494 by Jean-Christophe Filliâtre

### Gilbreath's card trick: split into a theory and a program

parent 7112d18b
 ... ... @@ -8,13 +8,13 @@ http://www.springerlink.com/content/gn18673357154448/ *) module GilbreathCardTrick theory GilbreathCardTrick use import int.Int use import list.List use import list.Append use import list.Reverse use import module stack.Stack use export int.Int use export list.List use export list.Length use export list.Append use export list.Reverse function m: int axiom m_positive: 0 < m ... ... @@ -38,7 +38,15 @@ module GilbreathCardTrick 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 forall a b c: list 'a. shuffle a b c -> length a + length b = length c end (* a program implementing the card trick using stacks *) module GilbreathCardTrick use import GilbreathCardTrick use import module stack.Stack let shuffle (a b: t int) = {} ... ...
 ... ... @@ -2,24 +2,6 @@ (* 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. ... ... @@ -28,6 +10,20 @@ 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) := ... ... @@ -44,20 +40,6 @@ Axiom Append_assoc : forall (a:Type), forall (l1:(list a)) (l2:(list a)) 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). ... ... @@ -93,19 +75,6 @@ Axiom reverse_reverse : forall (a:Type), forall (l:(list a)), 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. ... ...
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!