http://d.hatena.ne.jp/m-hiyama/20081024/1224814465 で紹介された、Seven Trees Puzzleの答えとなる全単射を、全単射であるという証明付きで構成する

Domain.v

(* definition of Tree *)
Inductive Tree : Set :=
  | leaf : Tree
  | node : Tree -> Tree -> Tree.

(* definition of Domain *)
Inductive Domain : Set :=
  | I : Domain
  | T : Domain
  | sum : Domain -> Domain -> Domain
  | prod : Domain -> Domain -> Domain.

Notation "t '+' u" := (sum t u).
Notation "t '*' u" := (prod t u).

Fixpoint Typeof (x : Domain) : Set :=
  match x with
  | I     => unit
  | T     => Tree
  | t + u => (Typeof t + Typeof u)%type
  | t * u => (Typeof t * Typeof u)%type
  end.

(* definition of DomainEq *)
Reserved Notation "t == u" (at level 70).

Inductive DomainEq : Domain -> Domain -> Type :=
  | eq_refl : forall a,          a == a
  | eq_symm : forall a b,        (a == b) -> b == a
  | eq_trans : forall a b c,     (a == b) -> (b == c) -> a == c

  | prod_intro : forall a b c d, (a == b) -> (c == d) -> a * c == b * d
  | prod_comm  : forall a b,     a * b == b * a
  | prod_assoc : forall a b c,   a * (b * c) == (a * b) * c
  | prod_unit  : forall a,       a * I == a

  | sum_intro : forall a b c d,  (a == b) -> (c == d) -> a + c == b + d
  | sum_comm  : forall a b,      a + b == b + a
  | sum_assoc : forall a b c,    a + (b + c) == (a + b) + c
  | distrib_l  : forall a b c,   a * (b + c) == a * b + a * c

  | expand_tree : T == I + T * T

where "t == u" := (DomainEq t u).

(* definition of Iso *)
Inductive Iso (X Y : Type) : Type :=
  | BijectionPair : forall (f : X -> Y), forall (f_inv: Y -> X),
      (forall x, x = f_inv (f x)) ->
      (forall x, x = f (f_inv x)) ->
      Iso X Y.

Definition bijection_from_iso {X Y : Type} (witness : Iso X Y) : X -> Y :=
  match witness with
    BijectionPair f _ _ _ => f
  end.

(* utility to write proof of DomainEq *)
Ltac Transform next_expr :=
  match goal with
  | [ |- _ == next_expr ]
    => idtac
  | [ |- _ == _ ]
    => apply (eq_trans _ next_expr _)
  end.

DomainEqToTypeIso.v

Require Import Coq.Program.Basics.
Require Export Domain.

Definition prod_swap {A B : Type} : (A * B) -> (B * A) :=
  fun x => match x with (a, b) => (b, a) end.

Ltac renameTypes :=
  match goal with 
  | [ a : Domain |- _] =>
       match goal with
       | [ta' := Typeof a |- _] => fail 1
       | _ => (* if there's no synonim for Typeof a, create it *)
              let ta := fresh "T" a
              in set (ta := (Typeof a))
       end
  end.

Ltac bij_pair f f_inv :=
  apply (BijectionPair _ _ f f_inv).

Theorem DomEq_then_Iso {x y : Domain} :
    x == y -> Iso (Typeof x) (Typeof y).
  intros wit.
  induction wit; simpl; repeat renameTypes.
  (* eq_refl *)
    bij_pair (fun x : Ta => x) (fun x : Ta => x).
    reflexivity.
    reflexivity.
  (* eq_symm *)
    destruct IHwit as [f f_inv Hf Hf'].
    bij_pair f_inv f.
    apply Hf'.
    apply Hf.
  (* eq_trans *)
    destruct IHwit1 as [fab fba Hab Hba].
    destruct IHwit2 as [fbc fcb Hcb Hbc].
    bij_pair (compose fbc fab) (compose fba fcb);
    unfold compose;
    intro x.
      rewrite <- Hcb.
      rewrite <- Hab.
      reflexivity.
      rewrite <- Hba.
      rewrite <- Hbc.
      reflexivity.
  (* prod_intro *)
    destruct IHwit1 as [fab fba Hab Hba].
    destruct IHwit2 as [fcd fdc Hcd Hdc].
    bij_pair
      (fun x => match x with (a, c) => (fab a, fcd c) end)
      (fun x => match x with (b, d) => (fba b, fdc d) end).
      destruct x.
      rewrite <- Hab; rewrite <- Hcd.
      reflexivity.
      destruct x.
      rewrite <- Hba; rewrite <- Hdc.
      reflexivity.
  (* prod_comm  *)
    bij_pair (@prod_swap Ta Tb) (@prod_swap Tb Ta);
      destruct x;
      reflexivity.
  (* prod_assoc *)
    bij_pair
      (fun x : Ta * (Tb * Tc) => match x with (a, bc) =>
                  match bc with (b, c) => ((a,b),c) end
                end)
      (fun x : Ta * Tb * Tc => match x with (ab, c) =>
                  match ab with (a, b) => (a, (b, c)) end
                end).
      destruct x as [xa [xb xc]].
      reflexivity.
      destruct x as [[xa xb] xc].
      reflexivity.
  (* prod_unit  *)
    bij_pair (fun x : Ta * unit => match x with (a, _) => a end)
             (fun a : Ta => (a, tt)).
      destruct x as [xa []].
      reflexivity.
      reflexivity.
  (* sum_intro *)
    destruct IHwit1 as [fab fba Hab Hba].
    destruct IHwit2 as [fcd fdc Hcd Hdc].
    bij_pair
      (fun x => match x with
                | inl a => inl (fab a)
                | inr c => inr (fcd c)
                end)
      (fun x => match x with
                | inl b => inl (fba b)
                | inr d => inr (fdc d)
                end).
     destruct x as [xa | xc].
       rewrite <- Hab; reflexivity.
       rewrite <- Hcd; reflexivity.
     destruct x as [xb | xd].
       rewrite <- Hba; reflexivity.
       rewrite <- Hdc; reflexivity.
  (* sum_comm  *)
    bij_pair
      (fun x : Ta + Tb => match x with
               | inl a => inr a
               | inr b => inl b
               end)
      (fun x : Tb + Ta => match x with
               | inl b => inr b
               | inr a => inl a
               end).
    destruct x; reflexivity.
    destruct x; reflexivity.
  (* sum_assoc *)
    bij_pair
      (fun x : Ta + (Tb + Tc) => match x with 
        | inl a => inl (inl a)
        | inr bc => match bc with
          | inl b => inl (inr b)
          | inr c => inr c
          end
        end)
      (fun x : Ta + Tb + Tc => match x with
        | inl ab => match ab with
          | inl a => inl a
          | inr b => inr (inl b)
          end
        | inr c => inr (inr c)
        end).
    destruct x as [xa|[xb|xc]]; reflexivity.
    destruct x as [[xa|xb]|xc]; reflexivity.
  (* distrib_l *)
    bij_pair
      (fun x : Ta * (Tb + Tc) => match x with (a, bc) =>
        match bc with
        | inl b => inl (a, b)
        | inr c => inr (a, c)
        end
      end)
      (fun x : Ta * Tb + Ta * Tc=> match x with
        | inl ab => match ab with (a, b) => (a, inl b) end
        | inr ac => match ac with (a, c) => (a, inr c) end
      end).
    destruct x as [xa[xb|xc]]; reflexivity.
    destruct x as [[xa xb] | [xa xc]]; reflexivity.
  (* expand_tree *)
     bij_pair
       (fun tree : Tree => match tree with
            | leaf       => inl tt
            | node t0 t1 => inr (t0, t1)
            end)
       (fun x : unit + Tree * Tree => match x with
            | inl _ => leaf
            | inr tpair => match tpair with (t0, t1) => node t0 t1 end
            end).
     destruct x; reflexivity.
     destruct x as [[]|[t0 t1]]; reflexivity.
Defined.

Definition bijection_from_domeq {x y : Domain} (witness : DomainEq x y) :
               (Typeof x) -> (Typeof y) :=
  bijection_from_iso (DomEq_then_Iso witness).

SevenTrees.v

Require Import Domain.
Require Import DomainEqToTypeIso.

Lemma sum_right :forall a b c, b == c -> a + b == a + c.
Proof.
  intros a b c H.
  apply sum_intro.
  apply eq_refl.
  apply H.
Defined.

Lemma sum_left : forall a b c, a == b -> a + c == b + c.
Proof.
  intros a b c H.
  apply sum_intro.
  apply H.
  apply eq_refl.
Defined.

Lemma split : forall a, a * T == a + a * T * T.
Proof.
  intros a.
  Transform (a * (I + T * T)).
    apply prod_intro.
      apply eq_refl.
      apply expand_tree.
  Transform (a * I + a * (T * T)).
    apply distrib_l.
  Transform (a + a * T * T).
    apply sum_intro.
      apply prod_unit.
      apply prod_assoc.
Defined.

Lemma merge : forall a, a + a * T * T == a * T.
Proof.
  intros a.
  apply eq_symm.
  apply split.
Defined.

Definition Invar (a : Domain) : Domain :=
  a + a * T * T * T.

Lemma Invar_add_T : forall a, Invar a == Invar (a * T).
Proof.
  intro a.
  unfold Invar.
  Transform (a + (a * T * T + a * T * T * T * T)).
    apply sum_right.
    apply split.
  Transform (a + a * T * T + a * T * T * T * T).
    apply sum_assoc.
  Transform (a * T + a * T * T * T * T).
    apply sum_left.
    apply merge.
Defined.

Lemma Invar_add_T4 : forall a, Invar a == Invar (a * T * T * T * T).
Proof.
  intro a.
  Transform (Invar (a * T)).
    apply Invar_add_T.
  Transform (Invar (a * T * T)).
    apply Invar_add_T.
  Transform (Invar (a * T * T * T)).
    apply Invar_add_T.
  Transform (Invar (a * T * T * T * T)).
    apply Invar_add_T.
Defined.

Fixpoint power (a : Domain) (n : nat) : Domain :=
  match n with
  | O    => I
  | S n' => (power a n') * a
  end.

Notation "a ^ n" := (power a n).

Theorem sevenTrees : T == T ^ 7.
Proof.
  Transform (T * I).
      apply eq_symm.
      apply prod_unit.
  Transform (T^1).
      apply prod_comm.
  Transform (T^0 + T^2).
      apply split.
  Transform (T^0 + (T^1 + T ^3)).
      apply sum_right.
      apply split.
  Transform (T^1 + (T^0 + T^3)).
      Transform ((T^0 + T^1) + T^3).
      apply sum_assoc.
      Transform ((T^1 + T^0) + T^3).
      apply sum_left.
      apply sum_comm.
      Transform (T^1 + (T^0 + T^3)).
      apply eq_symm.
      apply sum_assoc.
  Transform (T^1 + (T^4 + T^7)).
      apply sum_right.
      replace (T^0 + T^3) with (Invar (T^0)) by reflexivity.
      replace (T^4 + T^7) with (Invar (T^4)) by reflexivity.
      apply Invar_add_T4.
  Transform ((T^1 + T^4) + T^7).
      apply sum_assoc.
  Transform ((T^5 + T^8) + T^7).
      apply sum_left.
      replace (T^1 + T^4) with (Invar (T^1)) by reflexivity.
      replace (T^5 + T^8) with (Invar (T^5)) by reflexivity.
      apply Invar_add_T4.
  Transform (T^5 + T^7 + T^8).
      Transform (T^5 + (T^8 + T^7)).
      apply eq_symm.
      apply sum_assoc.
      Transform (T^5 + (T^7 + T^8)).
      apply sum_right.
      apply sum_comm.
      Transform (T^5 + T^7 + T^8).
      apply sum_assoc.
  Transform (T^6 + T^8).
      apply sum_left.
      apply merge.
  Transform (T^7).
      apply merge.
Defined.

Definition TtoT7 : (Typeof T) -> (Typeof (T^7)) :=
   bijection_from_domeq sevenTrees.

Definition T7toT : (Typeof (T^7)) -> (Typeof T) :=
   bijection_from_domeq (eq_symm _ _ sevenTrees).


(* example *)
Let theTree := node leaf (node (node leaf leaf) leaf).
Let trees := let t1 := (tt, theTree)
             in let t2 := (t1, theTree)
             in let t3 := (t2, theTree)
             in let t4 := (t3, theTree)
             in let t5 := (t4, theTree)
             in let t6 := (t5, theTree)
             in (t6, theTree).
Goal theTree = T7toT (TtoT7 theTree).
Proof. reflexivity. Qed.

Goal trees = TtoT7 (T7toT trees).
Proof. reflexivity. Qed.