Require Import Coq.Logic.ProofIrrelevance.
Require Import Coq.omega.Omega.
Require Import Logic.lib.Bijection.
Require Import Logic.lib.Countable.
Require Import Logic.GeneralLogic.Base.
Require Import Logic.MinimunLogic.Syntax.

Local Open Scope logic_base.
Local Open Scope syntax.

Inductive expr {Var: Type}: Type :=
  | impp : expr -> expr -> expr
  | varp : Var -> expr.

Arguments expr Var: clear implicits.

Instance L (Var: Type): Language :=
  Build_Language (expr Var).

Instance minL (Var: Type): MinimunLanguage (L Var) :=
  Build_MinimunLanguage (L Var) impp.

Definition rank {Var: Type}: expr Var -> nat :=
  fix rank (x: expr Var): nat :=
    match x with
    | impp y z => 1 + rank y + rank z
    | varp p => 0
    end.

Definition formula_countable: forall Var, Countable Var -> Countable (expr Var).
(* Goal: forall (Var : Type) (_ : Countable Var), Countable (expr Var) *)
  intros.
(* Goal: Countable (expr Var) *)
  assert (forall n, Countable (sig (fun x: expr Var => rank x <= n))).
  + induction n.
    - apply (@bijection_Countable _ Var); [| solve_Countable].
(* Goal: bijection (@sig (expr Var) (fun x : expr Var => le (@rank Var x) O)) Var *)
      apply bijection_sym.
(* Goal: bijection Var (@sig (expr Var) (fun x : expr Var => le (@rank Var x) O)) *)
      apply (FBuild_bijection _ _ (fun p => exist (fun x: expr Var => rank x <= 0) (varp p) (le_n 0))).
(* Goal: forall (Var : Type) (_ : Countable Var), Countable (expr Var) *)
      * hnf; intros.
(* Goal: @eq (expr Var) a1 a2 *)
        inversion H; auto.
(* Goal: forall (Var : Type) (_ : Countable Var), Countable (expr Var) *)
      * hnf; intros.
(* Goal: @ex Var (fun a : Var => @eq (@sig (expr Var) (fun x : expr Var => le (@rank Var x) O)) (@exist (expr Var) (fun x : expr Var => le (@rank Var x) O) (@varp Var a) (le_n O)) b) *)
        destruct b as [[] HH]; try solve [inversion HH].
(* Goal: @ex Var (fun a : Var => @eq (@sig (expr Var) (fun x : expr Var => le (@rank Var x) O)) (@exist (expr Var) (fun x : expr Var => le (@rank Var x) O) (@varp Var a) (le_n O)) (@exist (expr Var) (fun x : expr Var => le (@rank Var x) O) (@varp Var v) HH)) *)
        exists v.
(* Goal: @eq (@sig (expr Var) (fun x : expr Var => le (@rank Var x) O)) (@exist (expr Var) (fun x : expr Var => le (@rank Var x) O) (@varp Var v) (le_n O)) (@exist (expr Var) (fun x : expr Var => le (@rank Var x) O) (@varp Var v) HH) *)
        eauto; f_equal; apply proof_irrelevance.
    - set (s := sig (fun x: expr Var => rank x <= n)).
      apply (@injection_Countable _ (s * s + Var)%type); [| solve_Countable].

      apply (Build_injection _ _ (fun x y =>
        match y with
        | inl (exist _ y _, exist _ z _) => proj1_sig x = impp y z
        | inr p => proj1_sig x = varp p
        end)).
(* Goal: forall (Var : Type) (_ : Countable Var), Countable (expr Var) *)
      * hnf; intros.
(* Goal: @ex (sum (prod (@sig (expr Var) (fun x : expr Var => le (@rank Var x) n)) (@sig (expr Var) (fun x : expr Var => le (@rank Var x) n))) Var) (fun b : sum (prod (@sig (expr Var) (fun x : expr Var => le (@rank Var x) n)) (@sig (expr Var) (fun x : expr Var => le (@rank Var x) n))) Var => match b with | inl (pair (exist _ y y3 as y1) (exist _ z y4 as y2) as y0) => @eq (expr Var) (@proj1_sig (expr Var) (fun x : expr Var => le (@rank Var x) (S n)) a) (@impp Var y z) | inr p => @eq (expr Var) (@proj1_sig (expr Var) (fun x : expr Var => le (@rank Var x) (S n)) a) (@varp Var p) end) *)
        destruct a as [[y z | p] ?H].
        (* 1 *) simpl in H. assert (rank y <= n) by omega. assert (rank z <= n) by omega.
(* Goal: @ex (sum (prod (@sig (expr Var) (fun x : expr Var => le (@rank Var x) n)) (@sig (expr Var) (fun x : expr Var => le (@rank Var x) n))) Var) (fun b : sum (prod (@sig (expr Var) (fun x : expr Var => le (@rank Var x) n)) (@sig (expr Var) (fun x : expr Var => le (@rank Var x) n))) Var => match b with | inl (pair (exist _ y3 y4 as y1) (exist _ z0 y5 as y2) as y0) => @eq (expr Var) (@proj1_sig (expr Var) (fun x : expr Var => le (@rank Var x) (S n)) (@exist (expr Var) (fun x : expr Var => le (@rank Var x) (S n)) (@impp Var y z) H)) (@impp Var y3 z0) | inr p => @eq (expr Var) (@proj1_sig (expr Var) (fun x : expr Var => le (@rank Var x) (S n)) (@exist (expr Var) (fun x : expr Var => le (@rank Var x) (S n)) (@impp Var y z) H)) (@varp Var p) end) *)
(* Goal: @ex (sum (prod (@sig (expr Var) (fun x : expr Var => le (@rank Var x) n)) (@sig (expr Var) (fun x : expr Var => le (@rank Var x) n))) Var) (fun b : sum (prod (@sig (expr Var) (fun x : expr Var => le (@rank Var x) n)) (@sig (expr Var) (fun x : expr Var => le (@rank Var x) n))) Var => match b with | inl (pair (exist _ y y3 as y1) (exist _ z y4 as y2) as y0) => @eq (expr Var) (@proj1_sig (expr Var) (fun x : expr Var => le (@rank Var x) (S n)) (@exist (expr Var) (fun x : expr Var => le (@rank Var x) (S n)) (@varp Var p) H)) (@impp Var y z) | inr p0 => @eq (expr Var) (@proj1_sig (expr Var) (fun x : expr Var => le (@rank Var x) (S n)) (@exist (expr Var) (fun x : expr Var => le (@rank Var x) (S n)) (@varp Var p) H)) (@varp Var p0) end) *)
                exists (inl (exist _ y H0, exist _ z H1)); auto.
        (* 2 *) exists (inr p); auto.
(* Goal: forall (Var : Type) (_ : Countable Var), Countable (expr Var) *)
      * hnf; intros.
        destruct a as [[y z | p] ?H];
        destruct b1 as [[[y1 ?H] [z1 ?H]] | p1]; try solve [inversion H];
        destruct b2 as [[[y2 ?H] [z2 ?H]] | p2]; try solve [inversion H0].
        (* 1 *) inversion H; inversion H0; subst; subst; repeat f_equal; apply proof_irrelevance.
        (* 2 *) inversion H; inversion H0; subst; subst; repeat f_equal; apply proof_irrelevance.
(* Goal: forall (Var : Type) (_ : Countable Var), Countable (expr Var) *)
      * hnf; intros.
        destruct b as [[[y ?H] [z ?H]] | p];
        destruct a1 as [[y1 z1 | p1] ?H]; try solve [inversion H];
        destruct a2 as [[y2 z2 | p2] ?H]; try solve [inversion H0].
        (* 1 *) inversion H; inversion H0; subst; subst; repeat f_equal; apply proof_irrelevance.
        (* 2 *) inversion H; inversion H0; subst; subst; repeat f_equal; apply proof_irrelevance.
  + apply (@injection_Countable _ (sigT (fun n => sig (fun x: expr Var => rank x <= n)))); [| solve_Countable; auto].
(* Goal: injection (expr Var) (@sigT nat (fun n : nat => @sig (expr Var) (fun x : expr Var => le (@rank Var x) n))) *)
    apply (FBuild_injection _ _ (fun x0 => existT (fun n => sig (fun x => rank x <= n)) (rank x0) (exist (fun x => rank x <= rank x0) x0 (le_n (rank x0))))).
(* Goal: forall (Var : Type) (_ : Countable Var), Countable (expr Var) *)
    hnf; intros.
(* Goal: @eq (expr Var) a1 a2 *)
    simpl in H.
(* Goal: @eq (expr Var) a1 a2 *)
    inversion H; auto.
Qed.

