Fooling Penn and Teller with permutations -- in F*

The Trick

In E807 of "Penn and Teller: Fool Us", the magician "Hans" fools P&T with the following trick:

1. He distributes large rock, piece of paper, and scissors to the three hosts/players, in order. Penn gets the rock, Teller gets the scissors, and Alyson gets the paper.
2. He makes a prediction, asks one person to choose a swap to make (among any of the three players). The players exchange props, and reveals "Teller beats Penn".
3. He makes a second prediction, asks two people to choose swaps to make, and reveals "Alyson beats teller, Penn beats Alyson".
4. He makes a third prediction, and asks each of the three people to choose a swap to make. On the prop piece of paper is his prediction "Teller beats Alyson, Penn beats Teller, Alyson beats Penn."

Penn and Teller guessed that Hans had multiple outs covering all possibilities. But the trick used another illusion, illustrated here using the dependently typed programming language https://www.fstar-lang.org/.

The Code

Let's define the players, as a type with three constructors.

type person = 
 | Penn
 | Teller
 | Alyson

let all_people = [Penn; Teller; Alyson]

We can also define the objects, the rules of rock-paper-scissors:

type object = 
 | Rock
 | Paper
 | Scissors

// The rules of rock-paper-scissors
let beats (o1:object) (o2:object) : bool =
  match o1 with
  | Rock -> o2 = Scissors
  | Paper -> o2 = Rock
  | Scissors -> o2 = Paper

We'll represent the objects each player is holding with a function, which must be injective. That is, no two players have the same object. (Because the function has finite domain, it must also be surjective, but I didn't include that.) We can describe that by putting a refinement on the type of the function, containing the extra condition.

// An assignment of person to object must be injective mapping
type assignment = (f:(person->object){forall x y. x <> y ==> f x <> f y})

Now, we can do our first "proof". It looks like a function-- one for determining which player is beaten by which other player. But it's a proof that there is always one, and exactly one. This is true because all three objects are out there, and each object beats some other object, but only one.

So, we filter the list of people based on whether the object they carry is beaten by the object "p" carries:

// Each player only beats one other player
// Prove that this is the case in the case of writing the function
let player_beats (a:assignment) (p:person) : (q:person{beats (a p) (a q)})  =
   let l = List.Tot.filter (fun (q:person) -> beats (a p) (a q)) all_people in
      // assert ( length l = 1 ); -- unnecessary, SMT figures it out!
      hd l

Note the refinement type on the return values, ensuring that the function picks somebody who is actually beaten. Under the hoods, F* calls out to a solver. In this case, its the Z3 solver, which understands sentences in the language of SMT -- logical Theories with Satisfiability, integer arithmetic, and other structures under a Modulus, a particular logical theory of equality.

We can define the starting state of the trick, although we will not need it. But we can verify that it is a valid assignment, as we defined it:

let start_assignment : assignment =
  fun p  -> match p with
  | Penn -> Rock
  | Teller -> Scissors
  | Alyson -> Paper

Now, I could not get a "good" version of the operation of transposing two objects to work, so I had to write it out in all its gory detail:

let transpose_assignment2 (a:assignment) (p1:person) (p2:person{p1 <> p2})  : assignment =
  match (p1,p2) with
  | (Penn,Teller) -> ( fun p -> match p with | Penn -> (a Teller) | Teller -> (a Penn) | Alyson -> (a Alyson) )
  | (Teller,Penn) -> ( fun p -> match p with | Penn -> (a Teller) | Teller -> (a Penn) | Alyson -> (a Alyson) )
  | (Penn,Alyson) -> ( fun p -> match p with | Penn -> (a Alyson) | Teller -> (a Teller) | Alyson -> (a Penn) )
  | (Alyson,Penn) -> ( fun p -> match p with | Penn -> (a Alyson) | Teller -> (a Teller) | Alyson -> (a Penn) )
  | (Teller,Alyson) -> ( fun p -> match p with | Penn -> (a Penn) | Teller -> (a Alyson) | Alyson -> (a Teller) )
  | (Alyson,Teller) -> ( fun p -> match p with | Penn -> (a Penn) | Teller -> (a Alyson) | Alyson -> (a Teller) )

This just says, for every possible pair of people, implement the match where those two players switch objects. If the old assignment a gave the scissors to Penn and the rock to Alyson then transpose_assignment2 a Penn Alyson would give a new assignment where Penn has the rock and Alyson has the scissors.

Spoilers

Stop here if you don't want the secret of the magic trick revealed. It's a theorem (a Lemma) in F*, which is just a special kind of function that is type-checked according to F*'s normal rules.

Photo by Yuvraj Singh on Unsplash

let theorem_all_transpositions_are_equivalent
 (x:assignment) (a1:person) (a2:person{a2<>a1}) 
 (b1:person) (b2:person{b1<>b2}) 
 // Any two transpositions result in the same player outcomes
 : Lemma (ensures (forall p1 .
       player_beats (transpose_assignment2 x a1 a2) p1 = 
       player_beats (transpose_assignment2 x b1 b2) p1)) =
   () 

This says that for any two transpositions, the new "prediction" of who beats who is exactly the same.

I was worried I would have to work hard to prove this! But I didn't, F* verified it was correct by giving it to the SMT solver, which was able to determine that it was true. So no further code was needed on my part.

I won't go further into the math, but you might draw the diagram of "X beats Y" and see what happens to it when two of the players switch objects.

Failed attempts

I initially wanted to write the transposition function something like this:

let other_person (p1:person) (p2:person{p1 <> p2}) : (p3:person{p1 <> p3 /\ p2 <> p3} ) =
  hd (List.Tot.filter (fun p -> p <> p1 && p <> p2) all_people)

let permute (a:assignment) 
  (p1:person) (p2:person{p1 <> p2}) (p3:person{p1 <> p3 /\ p2 <> p3})
  (q1:person) (q2:person{p1 <> p2}) (q3:person{p1 <> p3 /\ p2 <> p3})
  : person->object =
  fun (x:person) -> match x with
    | p1 -> (a q1)
    | p2 -> (a q2)
    | p3 -> (a q3)

let transpose_assignment (a:assignment) (p1:person) (p2:person{p1 <> p2})  : assignment =
  let p3 = other_person p1 p2 in 
    permute a p1 p2 p3 p2 p1 p3

This defines a general way of writing permutations of the person-to-object mapping, and uses it to implement a simple transposition, by identifying who the third player is (who keeps their object.)

The first function works fine. Once again F* is successfully able to prove that filtering two people out of the list leaves exactly one.

But, I am not able to convince it that the permutation is also a valid assignment. I think this is because the knowledge that the three players are all the possibilities is not encoded in the correct way.

I tried proving it as a theorem:

let permute_is_assignment (a:assignment)
  (p1:person) (p2:person{p1 <> p2}) (p3:person{p1 <> p3 /\ p2 <> p3})
  (q1:person) (q2:person{p1 <> p2}) (q3:person{p1 <> p3 /\ p2 <> p3}) 
  : Lemma( forall (x:person) (y:person). x <> y ==> (permute a p1 p2 p3 q1 q2 q3)  x <> (permute a p1 p2 p3 q1 q2 q3) y )
  = let foo (x:person) (y:person) : Lemma (x <> y ==> (permute a p1 p2 p3 q1 q2 q3)  x <> (permute a p1 p2 p3 q1 q2 q3) y) = 
      let bar (ne:(x <> y)) : Lemma ((permute a p1 p2 p3 q1 q2 q3)  x <> (permute a p1 p2 p3 q1 q2 q3) y) = 
         match (x,y) with 
         | (p1, p2) -> assert( x <> y  ); assert (p1 <> p2 ); assert( x <> p3 ); ()
         | (p1, p3) -> admit()
         | (p2, p1) -> admit()
         | (p2, p3) -> admit()
         | (p3, p1) -> admit()
         | (p3, p2) -> admit()         
      in FStar.Classical.impl_intro bar
    in  
    FStar.Classical.forall_intro_2 foo

This breaks down the proof into smaller pieces, basically mirroring the structure of the assertion we want to prove. The admit() calls are placeholders; I used them to verify with F* that if I could fill in each case, then the proof would be valid. And F* verifies that the cases I listed in the match expression are all the ones that are possible.

But, the code fails on assert (x <> p3 ); It should be the case that if x = p1, and p3 <> p1, then x <> p3, but somehow that is getting lost. F* uses <> for "not equals."

So, I would need to find a way to fix this either by changing how I represented the players, or changing the refinement types, or proving an appropriate lemma that lets F* know what I know.

Links

The full code for this example is at https://github.com/mgritter/aoc-fstar/blob/main/other/PennAndTeller.fst

This December, you can watch me solve Advent of Code problems in F* on my Twitch channel:

To learn more about F*, consider reading the old tutorial (a new one is in the works but is not complete!): https://fstar-lang.org/tutorial/tutorial.html