Require Export PropiLmodel.

Fixpoint HarropF u: Prop :=
  match u with
    | Var _ ⇒ True
    | Fal ⇒ True
    | Imp s t ⇒ HarropF t
    | And s t ⇒ HarropF s ∧ HarropF t
    | Or s t ⇒ False
  end.

Definition HarropC A: Prop := ∀ s, s el A → HarropF s.

Lemma Harrop A p q: HarropC A → gen A (Or p q) ↔ gen A p ∨ gen A q.

Lemma OrFree_Harrop s: OrFree s → HarropF s.

Lemma genXM x:
  ¬ gen [] (Or (Var x) (Not (Var x))).

Lemma OrIndependence p q:
   ¬ (gen [p] q ∨ gen [q] p)
   → ¬ ∃ s, OrFree s ∧ gen [] (Equi (Or p q) s).

(* The results are from
  McKinsey, J. C. C. (1939). Proof of the independence of the primitive symbols
  of Heyting's calculus of propositions. Journal of Symbolic Logic 4 (4):155-158
*)

Section HeytingHMK1.
  (* McKinsey's Matrix I to prove undefinability of Fal *)

  (* Lattice:
      top
       |
       |
       a
       |
       |
      bot
  *)

  Inductive HMK1: Type := HMK1bot | HMK1a | HMK1top.

  Definition HMK1R (a b: HMK1) : Prop :=
    match a,b with
      | HMK1bot, _ ⇒ True
      | _, HMK1bot ⇒ False
      | _, HMK1top ⇒ True
      | HMK1top, _ ⇒ False
      | HMK1a, HMK1a ⇒ True
    end.

  Definition HMK1meet (a b: HMK1) : HMK1 :=
    match a,b with
      | HMK1bot, _ ⇒ HMK1bot
      | _ , HMK1bot ⇒ HMK1bot
      | HMK1top, b ⇒ b
      | a, HMK1top ⇒ a
      | HMK1a, HMK1a ⇒ HMK1a
    end.

  Definition HMK1join (a b: HMK1) : HMK1 :=
    match a,b with
      | HMK1top, _ ⇒ HMK1top
      | _, HMK1top ⇒ HMK1top
      | HMK1bot, b ⇒ b
      | a, HMK1bot ⇒ a
      | HMK1a, HMK1a ⇒ HMK1a
    end.

  Definition HMK1imp (a b : HMK1) : HMK1 :=
    match a,b with
      | HMK1bot, _ ⇒ HMK1top
      | _, HMK1top ⇒ HMK1top
      | _, HMK1bot ⇒ HMK1bot
      | HMK1top, b ⇒ b
      | HMK1a, HMK1a ⇒ HMK1top
    end.

  Lemma HMK1Rref a: HMK1R a a.

  Lemma HMK1Rtra a b c: HMK1R a b → HMK1R b c → HMK1R a c.

  Definition HMK1HA : HeytingAlgebra.

  (* Fal is undefinable by other connectives *)
  Lemma FalIndependence_hey:
    ¬ ∃ s, FalFree s ∧ nd [] (Equi s Fal).

End HeytingHMK1.

Section HeytingHMK2.
  (* McKinsey's Matrix II to prove undefinability of Or *)

  (* Lattice: 
                        top
                         |
                         |
                      a \/ b
                     /      \
                    a        b
                     \      /
                      \    /
                       bot
  *)

  Inductive HMK2 : Type := HMK2bot | HMK2a | HMK2b | HMK2ab | HMK2top.

  Definition HMK2R (a b: HMK2) : Prop :=
    match a,b with
      | HMK2bot, _ ⇒ True
      | _, HMK2bot ⇒ False
      | _, HMK2top ⇒ True
      | HMK2top, _ ⇒ False
      | HMK2a, HMK2a ⇒ True
      | HMK2a, HMK2b ⇒ False
      | HMK2a, HMK2ab ⇒ True
      | HMK2b, HMK2a ⇒ False
      | HMK2b, HMK2b ⇒ True
      | HMK2b, HMK2ab ⇒ True
      | HMK2ab, HMK2a ⇒ False
      | HMK2ab, HMK2b ⇒ False
      | HMK2ab, HMK2ab ⇒ True
    end.

  Definition HMK2meet (a b: HMK2) : HMK2 :=
    match a,b with
      | HMK2bot, _ ⇒ HMK2bot
      | _, HMK2bot ⇒ HMK2bot
      | HMK2top, b ⇒ b
      | a, HMK2top ⇒ a
      | HMK2a, HMK2a ⇒ HMK2a
      | HMK2a, HMK2b ⇒ HMK2bot
      | HMK2a, HMK2ab ⇒ HMK2a
      | HMK2b, HMK2a ⇒ HMK2bot
      | HMK2b, HMK2b ⇒ HMK2b
      | HMK2b, HMK2ab ⇒ HMK2b
      | HMK2ab, b ⇒ b
    end.

  Definition HMK2join (a b: HMK2) : HMK2 :=
    match a,b with
      | HMK2bot, b ⇒ b
      | a, HMK2bot ⇒ a
      | HMK2top, _ ⇒ HMK2top
      | _, HMK2top ⇒ HMK2top
      | _, HMK2ab ⇒ HMK2ab
      | HMK2ab, _ ⇒ HMK2ab
      | HMK2a, HMK2a ⇒ HMK2a
      | HMK2a, HMK2b ⇒ HMK2ab
      | HMK2b, HMK2a ⇒ HMK2ab
      | HMK2b, HMK2b ⇒ HMK2b
    end.

  Definition HMK2imp (a b: HMK2) : HMK2 :=
    match a,b with
      | HMK2bot, _ ⇒ HMK2top
      | _, HMK2top ⇒ HMK2top
      | HMK2a, HMK2bot ⇒ HMK2b
      | HMK2a, HMK2a ⇒ HMK2top
      | HMK2a, HMK2b ⇒ HMK2b
      | HMK2a, HMK2ab ⇒ HMK2top
      | HMK2b, HMK2bot ⇒ HMK2a
      | HMK2b, HMK2a ⇒ HMK2a
      | HMK2b, HMK2b ⇒ HMK2top
      | HMK2b, HMK2ab ⇒ HMK2top
      | HMK2ab, HMK2bot ⇒ HMK2bot
      | HMK2ab, HMK2a ⇒ HMK2a
      | HMK2ab, HMK2b ⇒ HMK2b
      | HMK2ab, HMK2ab ⇒ HMK2top
      | HMK2top, b ⇒ b
    end.

  Lemma HMK2Rref a: HMK2R a a.

  Lemma HMK2Rtra a b c: HMK2R a b → HMK2R b c → HMK2R a c.

  Definition HMK2HA : HeytingAlgebra.

  Lemma OrIndependence_hey:
    ¬ ∃ s, OrFree s ∧ nd [] (Equi (Or (Var 0) (Var 1)) s).

End HeytingHMK2.

Section HeytingHMK3.
  (* McKinsey's Matrix III to prove undefinability of Imp and And *)

  (* Matrix III is actually the direct product of Matrix I with itself *)
  (* Lattice: 1-top 2-a 3-bot
                        11
                       /  \
                      12  21
                     /  \/  \
                    13  22  31
                     \  /\  /
                      23  32
                       \  /
                        33
  *)

  Definition HMK3: Type := prod HMK1 HMK1.

  Definition HMK3R (a b: HMK3) : Prop :=
    match a, b with
      | (a1,a2), (b1, b2) ⇒ HMK1R a1 b1 ∧ HMK1R a2 b2
    end.

  Definition HMK3meet (a b: HMK3) : HMK3 :=
    match a, b with
      | (a1,a2), (b1, b2) ⇒ (HMK1meet a1 b1, HMK1meet a2 b2)
    end.

  Definition HMK3join (a b: HMK3) : HMK3 :=
    match a, b with
      | (a1,a2), (b1, b2) ⇒ (HMK1join a1 b1, HMK1join a2 b2)
    end.

  Definition HMK3imp (a b: HMK3) : HMK3 :=
    match a, b with
      | (a1,a2), (b1, b2) ⇒ (HMK1imp a1 b1, HMK1imp a2 b2)
    end.

  Lemma HMK3Rref a: HMK3R a a.

  Lemma HMK3Rtra a b c: HMK3R a b → HMK3R b c → HMK3R a c.

  Definition HMK3HA : HeytingAlgebra.

  (* Idea: Fal, Or, And are closed on {11, 12, 22, 33}, but 11->22 = 21 
     where 1-top 2-a 3-bot *)
  Lemma ImpIndependence_hey:
    ¬ ∃ s, ImpFree s ∧ nd [] (Equi (Imp (Var 0) (Var 1)) s).

    (* Idea: Fal, Or, Imp are closed on {11, 12, 13, 31, 33}, but 12/\31 = 32
     where 1-top 2-a 3-bot *)
  Lemma AndIndependence_hey:
    ¬ ∃ s, AndFree s ∧ nd [] (Equi (And (Var 0) (Var 1)) s).

End HeytingHMK3.

Lemma ndXM_hey x:
  ¬ nd [] (Or (Var x) (Not (Var x))).

Lemma ndDN_hey x:
  ¬ nd [] (Imp (Not (Not (Var x))) (Var x)).

Lemma ndDN'_hey x:
  ¬ nd [] (Or (Not (Var x)) (Not (Not (Var x)))).

Lemma ndDeMorgan_hey:
  ¬ nd [] (Imp (Not (And (Var 0) (Var 1))) (Or (Not (Var 0)) (Not (Var 1)))).