module Gilbreath where -- From the paper by Gerard Huet "The Gilbreath Trick: A case study in -- axiomatisation and proof development in the Coq proof assistant" -- Original formalisation in Coq v5.6, Technical report 1511, September 1991 -- Some modifications were done though. open import Data.Empty open import Data.Product open import Data.Sum open import Data.Bool open import Data.List open import Relation.Nullary.Core using (¬_) open import Relation.Binary.PropositionalEquality If_Then_Else : ∀ P Q R → Set If P Then Q Else R = (P × Q) ⊎ (¬ P × R) -- BOOLEANS not-intro : ∀ b → not (not b) ≡ b not-intro true = refl not-intro false = refl not-elim : ∀ b → b ≡ not (not b) not-elim b = sym (not-intro b) -- BOOLEAN WORDS: Deck of cards Deck : Set Deck = List Bool -- Concatenation of decks and properties data Concat : Deck → Deck → Deck → Set where conc-emp : ∀ dk → Concat [] dk dk conc-cons : ∀ dd dc dk → (b : Bool) → Concat dd dc dk → Concat (b ∷ dd) dc (b ∷ dk) -- ALTERNATING WORDS: Decks of alternating cards and properties -- Alter b dk if dk ≡ [b, not b, not (not b), ..] data Alter : Bool → Deck → Set where alt-emp : ∀ b → Alter b [] alt-cons : ∀ {b} → ∀ {dk} → Alter (not b) dk → Alter b (b ∷ dk) data Alternate : Deck → Set where alternate : ∀ {b} → ∀ {dk} → Alter b dk → Alternate dk alter2head-eq : ∀ {b d} → ∀ {dk} → Alter b (d ∷ dk) → b ≡ d alter2head-eq (alt-cons p) = refl alter2head-tail : ∀ {b d} → ∀ {dk} → Alter b (d ∷ dk) → b ≡ d × Alter (not b) dk alter2head-tail (alt-cons p) = (refl , p) alter-not-elim : ∀ {b d} → ∀ {dk} → Alter (not b) (d ∷ dk) → Alter b dk alter-not-elim {true} (alt-cons p) = p alter-not-elim {false} (alt-cons p) = p alter-not-intro : ∀ {b d} → ∀ {dk} → Alter b (d ∷ dk) → Alter (not b) dk alter-not-intro (alt-cons p) = p -- PARITY OF WORDS: Odd and Even and properties data Odd : Deck → Set where odd-sgl : ∀ b → Odd [ b ] odd-cons : ∀ b d → ∀ {dk} → Odd dk → Odd (b ∷ (d ∷ dk)) data Even : Deck → Set where even-emp : Even [] even-cons : ∀ b d → ∀ {dk} → Even dk → Even (b ∷ (d ∷ dk)) odd-even : ∀ b → ∀ {dk} → Odd dk → Even (b ∷ dk) odd-even b (odd-sgl d) = even-cons b d even-emp odd-even b (odd-cons d e p) = even-cons b d (odd-even e p) even-odd : ∀ b → ∀ {dk} → Even dk → Odd (b ∷ dk) even-odd b even-emp = odd-sgl b even-odd b (even-cons d e p) = odd-cons b d (even-odd e p) -- Odd and Even are disjoint properties not-odd-and-even : ∀ {dk} → Odd dk → Even dk → ⊥ not-odd-and-even (odd-sgl b) () not-odd-and-even (odd-cons b d po) (even-cons .b .d pe) = not-odd-and-even po pe odd-or-even : ∀ dk → Odd dk ⊎ Even dk odd-or-even [] = inj₂ even-emp odd-or-even (d ∷ []) = inj₁ (odd-sgl d) odd-or-even (b ∷ d ∷ dk) with odd-or-even dk ... | inj₁ p = inj₁ (odd-cons b d p) ... | inj₂ p = inj₂ (even-cons b d p) odd-even-concat : ∀ {dd} {dc} {dk} → Concat dd dc dk → (Odd dk × ((Odd dd × Even dc) ⊎ (Even dd × Odd dc))) ⊎ (Even dk × ((Odd dd × Odd dc) ⊎ (Even dd × Even dc))) odd-even-concat {[]} {.dk} {dk} (conc-emp .dk) with odd-or-even dk ... | inj₁ h = inj₁ (h , inj₂ (even-emp , h)) ... | inj₂ h = inj₂ (h , inj₂ (even-emp , h)) odd-even-concat {d ∷ dd} {dc} {.(d ∷ dk)} (conc-cons .dd .dc dk .d p) with odd-even-concat p ... | inj₁ (ok , inj₁ (od , ec)) = inj₂ (odd-even d ok , inj₂ (odd-even d od , ec)) ... | inj₁ (ok , inj₂ (ed , oc)) = inj₂ (odd-even d ok , inj₁ (even-odd d ed , oc)) ... | inj₂ (ek , inj₁ (od , oc)) = inj₁ (even-odd d ek , inj₂ (odd-even d od , oc)) ... | inj₂ (ek , inj₂ (ed , ec)) = inj₁ (even-odd d ek , inj₁ (even-odd d ed , ec)) even-concat : ∀ {dd dc dk} → Concat dd dc dk → Even dk → (Odd dd × Odd dc) ⊎ (Even dd × Even dc) even-concat p ek with odd-even-concat p ... | inj₁ (ok , h) = ⊥-elim (not-odd-and-even ok ek) ... | inj₂ (_ , h) = h -- Subwords of alternating words are alternating alter-concat-l : ∀ {b} → ∀ {dd dc dk} → Concat dd dc dk → Alter b dk → Alter b dd alter-concat-l {b} {[]} {dc} {dk} p q = alt-emp b alter-concat-l {b} {d ∷ dd} {dc} {.(d ∷ dk)} (conc-cons .dd .dc dk .d p) q with alter2head-tail q alter-concat-l {.d} {d ∷ dd} {dc} {.(d ∷ dk)} (conc-cons .dd .dc dk .d p) q | (refl , h) = alt-cons (alter-concat-l p h) alter-concat-r : ∀ {b} → ∀ {dd dc dk} → Concat dd dc dk → Alter b dk → (Odd dd × Alter (not b) dc) ⊎ (Even dd × Alter b dc) alter-concat-r {b} {[]} {.dk} {dk} (conc-emp .dk) q = inj₂ (even-emp , q) alter-concat-r {.d} {d ∷ dd} {dc} {.(d ∷ dk)} (conc-cons .dd .dc dk .d p) (alt-cons q) with alter-concat-r p q ... | inj₁ (od , h) = inj₂ (odd-even d od , subst (λ e → Alter e dc) (not-intro d) h) ... | inj₂ (ed , h) = inj₁ (even-odd d ed , h) -- OPPOSITE WORDS: Opposite decks start with different booleans data Opposite : Deck → Deck → Set where opp : ∀ b → ∀ dc dk → Opposite (b ∷ dc) ((not b) ∷ dk) not-opp-emp-l : ∀ dk → ¬(Opposite [] dk) not-opp-emp-l dk () not-opp-emp-r : ∀ dk → ¬(Opposite dk []) not-opp-emp-r dk () not-opp-same : ∀ b → ∀ dc dk → ¬(Opposite (b ∷ dc) (b ∷ dk)) not-opp-same true dc dk () not-opp-same false dc dk () -- The odd parts are there to ensure dc and dk are not empty opposite1 : ∀ {b} → ∀ {dc dk} → Odd dc → Alter b dc → Odd dk → Alter (not b) dk → Opposite dc dk opposite1 {b} {[]} {dk} () p ok q opposite1 {b} {d ∷ dc} {[]} oc p () q opposite1 {b} {d ∷ dc} {e ∷ dk} oc p ok q with alter2head-eq p | alter2head-eq q opposite1 {b} {.b ∷ dc} {.(not b) ∷ dk} oc p ok q | refl | refl = opp b dc dk opposite2 : ∀ {b} → ∀ {dc dk} → Alter b dc → Alter b dk → ¬(Opposite dc dk) opposite2 {b} {[]} {dk} p q = not-opp-emp-l dk opposite2 {b} {d ∷ dc} {[]} p q = not-opp-emp-r _ opposite2 {b} {d ∷ dc} {e ∷ dk} p q with alter2head-eq p | alter2head-eq q opposite2 {b} {.b ∷ dc} {.b ∷ dk} p q | refl | refl = not-opp-same b _ _ -- PAIRED WORDS: of the form [not b1, b1, not b2, b2, ..., not bn, bn ] data Paired : Deck → Set where paired-emp : Paired [] paired-cons : ∀ b → ∀ {dk} → Paired dk → Paired (not b ∷ (b ∷ dk)) {- -- An even alternating deck is paired even-alter2paired : ∀ {b} → ∀ {dk} → Even dk → Alter (not b) dk → Paired dk even-alter2paired even-emp p = paired-emp even-alter2paired {b} {.(not b ∷ e ∷ dk)} (even-cons .(not b) e {dk} ek) (alt-cons p) with alter2head-eq p even-alter2paired {b} {.(not b ∷ (not (not b)) ∷ dk)} (even-cons .(not b) .(not (not b)) {dk} ek) (alt-cons p) | refl = let adk : Alter (not b) dk adk = alter-not-intro (subst (λ a → Alter a (not (not b) ∷ dk)) (not-intro b) p) pdk : Paired (not b ∷ (b ∷ dk)) pdk = paired-cons b (even-alter2paired ek adk) in subst (λ a → Paired (not b ∷ a ∷ dk)) (not-elim b) pdk -} -- Rotating decks: rotate [b1, b2, .., bn] = [b2, .., bn, b1] rotate : Deck → Deck rotate [] = [] rotate (d ∷ dk) = dk ++ [ d ] -- A deck is PairedRot iff rotating it 1 position makes it paired -- PairedRot b w <=> w = [b, not b1, b1, not b2, b2, ..., not bn, bn , not b] data PairedRot : Bool → Deck → Set where prot-emp : ∀ b → PairedRot b [] prot-cons : ∀ {b} → ∀ {dk} → Paired (dk ++ [ b ]) → PairedRot b (b ∷ dk) paired-rotate : ∀ {b} → ∀ {dk} → PairedRot b dk → Paired (rotate dk) paired-rotate (prot-emp b) = paired-emp paired-rotate (prot-cons p) = p paired-r-from-rot : ∀ {b} → ∀ {dk} → PairedRot b dk → Paired (not b ∷ dk ++ [ b ]) paired-r-from-rot (prot-emp b) = paired-cons b paired-emp paired-r-from-rot (prot-cons {b} p) = paired-cons b p paired-r-from-rot-not : ∀ {b} → ∀ {dk} → PairedRot (not b) dk → Paired (b ∷ dk ++ [ not b ]) paired-r-from-rot-not {true} (prot-emp .false) = paired-cons _ paired-emp paired-r-from-rot-not {false} (prot-emp .true) = paired-cons _ paired-emp paired-r-from-rot-not {true} (prot-cons p) = paired-cons _ p paired-r-from-rot-not {false} (prot-cons p) = paired-cons _ p -- A deck is PairedBet iff -- is obtained by prefixing and suffixing a paired deck with the same boolean -- PairedBet b w <=> w = [b, not b1, b1, not b2, b2, ..., not bn, bn, not b] data PairedBet : Bool → Deck → Set where pbet-cons : ∀ {b} → ∀ {dk} → Paired (dk ++ [ not b ]) → PairedBet b (b ∷ dk) paired-r-from-bet : ∀ {b} → ∀ {dk} → PairedBet (not b) dk → Paired (b ∷ dk ++ [ b ]) paired-r-from-bet {true} (pbet-cons p) = paired-cons _ p paired-r-from-bet {false} (pbet-cons p) = paired-cons _ p paired-r-from-bet-not : ∀ {b} → ∀ {dk} → PairedBet b dk → Paired (not b ∷ dk ++ [ not b ]) paired-r-from-bet-not (pbet-cons p) = paired-cons _ p -- SHUFFLING DECKS data Shuffle : Deck → Deck → Deck → Set where shuffle-emp : Shuffle [] [] [] shuffle-cons-l : ∀ b → ∀ {dd dc dk} → Shuffle dd dc dk → Shuffle (b ∷ dd) dc (b ∷ dk) shuffle-cons-r : ∀ b → ∀ {dd dc dk} → Shuffle dd dc dk → Shuffle dd (b ∷ dc) (b ∷ dk) shuffling : ∀ {b} → ∀ {dd dc dk} → Shuffle dd dc dk → Alter b dd → (Odd dd × ((Odd dc × (Alter (not b) dc → Paired dk) × (Alter b dc → PairedBet b dk)) ⊎ (Even dc × (Alter b dc → Paired (not b ∷ dk)) × (Alter (not b) dc → Paired (dk ++ [ not b ]))))) ⊎ (Even dd × ((Odd dc × (Alter (not b) dc → Paired (dk ++ [ b ])) × (Alter b dc → Paired (not b ∷ dk))) ⊎ (Even dc × (Alter b dc → PairedRot b dk) × (Alter (not b) dc → Paired dk)))) -- both decks empty shuffling {b} shuffle-emp _ = inj₂ (even-emp , inj₂ (even-emp , ((λ h → prot-emp b) , λ h → paired-emp))) -- dd goes first: Shuffle (d :: dd) dc (d :: dk) shuffling {dd = d ∷ dd} {dk = .d ∷ dk} (shuffle-cons-l .d sd) al with alter2head-eq al | shuffling sd (alter-not-intro al) ... | refl | inj₁ (Odd , inj₁ (Odc , (hnb , hb))) = inj₂ (odd-even d Odd , inj₁ (Odc , ((λ h → paired-r-from-bet (hb h)) , λ h → paired-cons _ (hnb (subst (λ a → Alter a _) (not-elim d) h))))) ... | refl | inj₁ (Odd , inj₂ (Edc , (hb , hnb))) = inj₂ (odd-even d Odd , inj₂ (Edc , ((λ h → prot-cons (r-not-not-elim {lk = dk} h hnb)) , λ h → l-not-not-elim h hb))) where r-not-not-elim : ∀ {e} → ∀ {lc lk} → Alter e lc → (Alter (not (not e)) lc → Paired (lk ++ [ not (not e) ])) → Paired (lk ++ [ e ]) r-not-not-elim {true} p hn = hn p r-not-not-elim {false} p hn = hn p l-not-not-elim : ∀ {e} → ∀ {lc lk} → Alter (not e) lc → (Alter (not e) lc → Paired (not (not e) ∷ lk)) → Paired (e ∷ lk) l-not-not-elim {true} p hn = hn p l-not-not-elim {false} p hn = hn p ... | refl | inj₂ (Edd , inj₁ (Odc , (hnb , hb))) = inj₁ (even-odd d Edd , inj₁ (Odc , ((λ h → l-not-not-elim h hb) , λ h → pbet-cons (hnb (subst (λ a → Alter a _) (not-elim d) h))))) where l-not-not-elim : ∀ {e} → ∀ {lc lk} → Alter (not e) lc → (Alter (not e) lc → Paired (not (not e) ∷ lk)) → Paired (e ∷ lk) l-not-not-elim {true} p hn = hn p l-not-not-elim {false} p hn = hn p ... | refl | inj₂ (Edd , inj₂ (Edc , (hb , hnb))) = inj₁ (even-odd d Edd , inj₂ (Edc , ((λ h → paired-cons _ (hnb (subst (λ a → Alter a _) (not-elim d) h))) , λ h → paired-r-from-rot-not (hb h)))) -- dc goes first: Shuffle dd (d :: dc) (d :: dk) shuffling (shuffle-cons-r d sc) al with shuffling sc al ... | inj₁ (Odd , inj₁ (Odc , (hnb , hb))) = inj₁ (Odd , inj₂ (odd-even d Odc , ((λ h → alter2paired h hnb) , λ h → alter-not2paired h hb))) where alter2paired : ∀ {e f} → ∀ {lc lk} → Alter e (f ∷ lc) → (Alter (not e) lc → Paired lk) → Paired (not e ∷ f ∷ lk) alter2paired p hne with alter2head-eq p ... | refl = paired-cons _ (hne (alter-not-intro p)) alter-not2paired : ∀ {e f} → ∀ {lc lk} → Alter (not e) (f ∷ lc) → (Alter e lc → PairedBet e lk) → Paired (f ∷ lk ++ [ not e ]) alter-not2paired p he with alter2head-eq p ... | refl = paired-r-from-bet-not (he (alter-not-elim p)) ... | inj₁ (Odd , inj₂ (Edc , (hb , hnb))) = inj₁ (Odd , inj₁ (even-odd d Edc , ((λ h → alter-not2paired h hb) , λ h → alter2paired h hnb))) where alter-not2paired : ∀ {e f} → ∀ {lc lk} → Alter (not e) (f ∷ lc) → (Alter e lc → Paired (not e ∷ lk)) → Paired (f ∷ lk) alter-not2paired p he with alter2head-eq p ... | refl = he (alter-not-elim p) alter2paired : ∀ {e f} → ∀ {lc lk} → Alter e (f ∷ lc) → (Alter (not e) lc → Paired (lk ++ [ not e ])) → PairedBet e (f ∷ lk) alter2paired p hne with alter2head-eq p ... | refl = pbet-cons (hne (alter-not-intro p)) ... | inj₂ (Edd , inj₁ (Odc , (hnb , hb))) = inj₂ (Edd , inj₂ (odd-even d Odc , ((λ h → alter2paired h hnb) , λ h → alter-not2paired h hb))) where alter2paired : ∀ {e f} → ∀ {lc lk} → Alter e (f ∷ lc) → (Alter (not e) lc → Paired (lk ++ [ e ])) → PairedRot e (f ∷ lk) alter2paired p hne with alter2head-eq p ... | refl = prot-cons (hne (alter-not-intro p)) alter-not2paired : ∀ {e f} → ∀ {lc lk} → Alter (not e) (f ∷ lc) → (Alter e lc → Paired (not e ∷ lk)) → Paired (f ∷ lk) alter-not2paired p he with alter2head-eq p ... | refl = he (alter-not-elim p) ... | inj₂ (Edd , inj₂ (Edc , (hb , hnb))) = inj₂ (Edd , inj₁ (even-odd d Edc , ((λ h → alter-not2paired h hb) , λ h → alter2paired h hnb))) where alter-not2paired : ∀ {e f} → ∀ {lc lk} → Alter (not e) (f ∷ lc) → (Alter e lc → PairedRot e lk) → Paired (f ∷ lk ++ [ e ]) alter-not2paired p he with alter2head-eq p ... | refl = paired-r-from-rot (he (alter-not-elim p)) alter2paired : ∀ {e f} → ∀ {lc lk} → Alter e (f ∷ lc) → (Alter (not e) lc → Paired lk) → Paired (not e ∷ f ∷ lk) alter2paired p hne with alter2head-eq p ... | refl = paired-cons _ (hne (alter-not-intro p)) -- MAIN THEOREM module Main (b : Bool) (dd dc dx dk : Deck) (ex : Even dx) (alt-dx : Alter b dx) (con : Concat dd dc dx) (shf : Shuffle dd dc dk) where alt-dd : Alter b dd alt-dd = alter-concat-l con alt-dx module CaseOdd (od : Odd dd) where odd-dc : Odd dc odd-dc with even-concat con ex ... | inj₁ (od , oc) = oc ... | inj₂ (ed , ec) = ⊥-elim (not-odd-and-even od ed) -- alt: ⊥-elim (not-even-dd ed) alt-dc : Alter (not b) dc alt-dc with alter-concat-r con alt-dx ... | inj₁ (od , ac) = ac ... | inj₂ (ed , _) = ⊥-elim (not-odd-and-even od ed) opp-dd-dc : Opposite dd dc opp-dd-dc = opposite1 od alt-dd odd-dc alt-dc paired-dk : Paired dk paired-dk with shuffling shf alt-dd ... | inj₁ (od , inj₁ (oc , (ap , apb))) = ap alt-dc ... | inj₁ (od , inj₂ (ec , (ap , anp))) = ⊥-elim (not-odd-and-even odd-dc ec) ... | inj₂ (ed , _) = ⊥-elim (not-odd-and-even od ed) -- end module CaseOdd module CaseEven (ed : Even dd) where even-dc : Even dc even-dc with even-concat con ex ... | inj₁ (od , oc) = ⊥-elim (not-odd-and-even od ed) -- alt: ⊥-elim (not-odd-dd od) ... | inj₂ (ed , ec) = ec alt-dc : Alter b dc alt-dc with alter-concat-r con alt-dx ... | inj₁ (od , _) = ⊥-elim (not-odd-and-even od ed) ... | inj₂ (ed , ac) = ac nopp-dd-dc : ¬ (Opposite dd dc) nopp-dd-dc p = opposite2 alt-dd alt-dc p paired-rot-dk : Paired (rotate dk) paired-rot-dk with shuffling shf alt-dd ... | inj₁ (od , _) = ⊥-elim (not-odd-and-even od ed) ... | inj₂ (ed , inj₁ (oc , (anp , ap))) = ⊥-elim (not-odd-and-even oc even-dc) ... | inj₂ (ed , inj₂ (ec , (apr , anp))) = paired-rotate (apr alt-dc) -- end module CaseEven opp-vs-paired : If (Opposite dd dc) Then (Paired dk) Else (Paired (rotate dk)) opp-vs-paired with odd-or-even dd ... | inj₁ od = let open CaseOdd od in inj₁ (opp-dd-dc , paired-dk) ... | inj₂ ed = let open CaseEven ed in inj₂ (nopp-dd-dc , paired-rot-dk) -- end module Main gilbreath-trick : ∀ {dd dc dx dk} → Even dx → Alternate dx → Concat dd dc dx → Shuffle dd dc dk → If (Opposite dd dc) Then (Paired dk) Else (Paired (rotate dk)) gilbreath-trick {dd} {dc} {dx} {dk} ex (alternate {b} p) conc shf = opp-vs-paired where open Main b dd dc dx dk ex p conc shf