(* This script was developed in Coq v8.1, using CoqIDE *)

Require Import String.

Inductive LCterm: Set :=
  | Var : string -> LCterm
  | Abs:  string -> LCterm -> LCterm
  | App: LCterm -> LCterm -> LCterm.

Require Import Ensembles.

Fixpoint FV(t: LCterm): Ensemble string :=
  match t with
    | Var x => Singleton string x
    | Abs x t1 => Subtract string (FV t1) x
    | App t1 t2 => Union string (FV t1) (FV t2)
  end.

(*unused
Definition  combinator(t: LCterm): Prop := FV(t) = Empty_set string.
unused*)

Fixpoint subs(x: string) (t: LCterm) (t': LCterm){struct t}: LCterm :=
  match t with
    | Var y => if string_dec y x then t' else t
    | Abs y t1 => if string_dec y x then t else Abs y (subs x t1 t')
    | App t1 t2 => App (subs x t1 t') (subs x t2 t')
  end.

Fixpoint reduce(t: LCterm): LCterm :=
  match t with
    | Var _ => t
    | Abs y t1 => Abs y (reduce t1)
    | App t1 t2 => match t1 with
                              | Abs x t11 => subs x t11 t2
                              | _ => t
                            end
  end.

Eval compute in (reduce (App (Abs "x" (Var "x"))(Abs "y" (Var "y")))).

Theorem eq_LCterms: (reduce (App (Abs "x" (Var "x"))(Abs "y" (Var "y")))) = Abs "y" (Var "y").
Proof.
  unfold reduce.
  unfold subs.
  (*need theorem or tactic here to show string_dec "x" "x" is true,rather than immediately resorting to trivial*)
  (* assert (string_dec "x" "x") did not work *)
  trivial.
Qed.



Lemma In_subtract: forall U: Type, forall x y: U, forall s: Ensemble U, x <> y /\ ~ In U (Subtract U s y) x -> ~ In U s x.
Proof.
  intros U x y s x_nin_s.
  elim x_nin_s.
  intros x_neq_y x_nin_ss.
  intuition.  (*simplifies 'not' to '-> False' and introduces H*)
  clear H0 H1.
  elim x_nin_ss.
  Require Import Classical_sets.
  apply Subtract_intro.
  exact H.
  intuition.
(*  apply (Subtract_inv U s y x x_nin_ss).
  intuition. (*simplifies 'not' to '-> False' and introduces H*)
  assert (x_in_s_neq_y: In U s x /\ y <> x).
  apply ((Subtract_inv U s y x) H).
  elim x_in_s_neq_y.
  intros x_in_s x_neq_y.
  elim x_nin_s.
  exact x_in_s.
*)
Qed.

Lemma FV_incr: forall x s: string, forall M: LCterm, x <> s -> ~ In string (FV (Abs s M)) x -> ~ In string (FV M) x.
Proof.
  intros x s M x_neq_s x_nin_fvabsm.
  unfold FV in x_nin_fvabsm.  fold FV in x_nin_fvabsm.
  apply (In_subtract string x s (FV M)).
  split.
  exact x_neq_s.
  exact x_nin_fvabsm.
Qed.

Lemma sym_neq: forall U: Type, forall x y: U, x <> y -> y <> x.
Proof.
  intros U x y x_neq_y.
  intuition.
Qed.

Lemma nin_union: forall U: Type, forall s1 s2: Ensemble U, forall x: U,
  ~ In U (Union U s1 s2) x -> ~ In U s1 x /\ ~ In U s2 x.
Proof.
  intros U s1 s2 x x_nin_union.
  intuition.
Qed.

Lemma subs_ninFVid: forall x: string, forall M N: LCterm,
  ~ In string (FV M) x -> subs x M N = M.
Proof.
  intros x M N x_nin_fvm.
  induction M.
    unfold subs.
    case (string_dec s x).
      intro s_eq_x.
      unfold FV in x_nin_fvm.
      assert False.
        Require Import Constructive_sets.
        apply (x_nin_fvm (Singleton_intro string s  x s_eq_x)).
      contradiction.
    intro s_neq_x; trivial.
    unfold subs; fold subs.
    case (string_dec s x).
      intro s_eq_x; trivial.
    intro s_neq_x.
    apply (sym_neq string s x) in s_neq_x.
    assert (subs_eq_M: subs x M N = M).
      apply IHM.
      apply (FV_incr x s M s_neq_x x_nin_fvm).
    rewrite subs_eq_M.
    trivial.
  unfold subs; fold subs.
  unfold FV in x_nin_fvm; fold FV in x_nin_fvm.
  apply (nin_union string (FV M1) (FV M2) x) in x_nin_fvm.
  elim x_nin_fvm.
  intros x_nin_fvm1 x_nin_fvm2.
  assert (subs_eq_M1: subs x M1 N = M1).
    apply IHM1.
    exact x_nin_fvm1.
  assert (subs_eq_M2: subs x M2 N = M2).
    apply IHM2.
    exact x_nin_fvm2.
  rewrite subs_eq_M1.
  rewrite subs_eq_M2.
  trivial.
Qed.

Lemma subs_abs: forall x y: string, forall M N: LCterm,
  x = y -> subs x (Abs y M) N = Abs y M.
Proof.
  intros x y M N x_eq_y.
  unfold subs; fold subs.
  case (string_dec y x).
  trivial.
  apply sym_eq in x_eq_y.
  contradiction.
Qed.

Lemma subs_abs_neq: forall x y: string, forall M N: LCterm,
  x <> y -> subs x (Abs y M) N = Abs y (subs x M N).
Proof.
  intros x y M N x_neq_y.
  unfold subs; fold subs.
  case (string_dec y x).
    intro x_eq_y.
    apply sym_eq in x_eq_y.
    contradiction.
  trivial.
Qed.

Lemma subs_lemma: forall x y: string, forall M N L: LCterm,
  x <>y -> ~ In string (FV L) x ->
  subs y (subs x M N) L = subs x (subs y M L) (subs y N L).
Proof.
  intros x y M N L x_neq_y x_nin_fvl.
(*  intuition. (*simplifies hypotheses x_neq_y and x_nin_fvl*)*)
  induction M.
    unfold subs; fold subs.
    case (string_dec s x).
      intro s_eq_x.
      case (string_dec s y).
        intro s_eq_y.
        assert (x_eq_y: x = y).
          assert (x_eq_s: x = s).
            apply (sym_eq s_eq_x).
          apply (trans_eq x_eq_s s_eq_y).
        contradiction.
      unfold subs at 2.
      case (string_dec s x).
        intros. trivial.
      contradiction.
    case (string_dec s y).
    intro s_eq_y.
    unfold subs at 1.
    case (string_dec s y).
      intros.
      apply sym_eq.
      apply (subs_ninFVid x L (subs y N L)).
      exact x_nin_fvl.
    contradiction.
    intros s_neq_y s_neq_x.
    unfold subs at 1.
    case (string_dec s y).
    contradiction.
    intro.
    unfold subs at 1.
    case (string_dec s x).
      contradiction.
    trivial.


    unfold subs; fold subs.
    case (string_dec s x).
      intro s_eq_x.
      case (string_dec s y).
        intro s_eq_y.
        assert (s1: subs y (Abs s M) L = Abs s M).
          apply (subs_abs y s M L).
          apply sym_eq in s_eq_y; assumption.
        rewrite s1.
        assert (s2: subs x (Abs s M) (subs y N L) = Abs s M).
          apply (subs_abs x s M (subs y N L)).
          apply sym_eq in s_eq_x; assumption.
        rewrite s2.
        trivial.
      intro s_neq_y.
      assert (s1: subs y (Abs s M) L = Abs s (subs y M L)).
        apply (subs_abs_neq y s M L).
        auto.
      rewrite s1.
      assert (s2: subs x (Abs s (subs y M L)) (subs y N L)  = Abs s (subs y M L)).
        apply (subs_abs x s (subs y M L) (subs y N L)).
        auto.
      rewrite s2.
      trivial.

    intros s_neq_x.
    case (string_dec s y).
      intro s_eq_y.
      assert (s1: subs y (Abs s (subs x M N)) L = Abs s (subs x M N)).
        apply (subs_abs y s (subs x M N) L).
        auto.
      rewrite s1.
      assert (s2: subs x (Abs s M) (subs y N L) = Abs s (subs x M (subs y N L))).
        apply (subs_abs_neq x s M (subs y N L)).
        auto.
      rewrite s2.


(*Here is where I was stuck. I wrote that I should:

      use freshness of s (variable convention), or y not in FV(N), as assumption. how? ask on coq-club.
*)

(*
      case (bool_dec In string (FV N) y).

      z <> x, y, s.
      subs z (Abs s (subs x M N)) L = Abs s (subs z (subs x M N) L)
      subs z (Abs s (subs x M (subs y N L)) L = Abs s (subs z (subs x M (subs y N L)) L)
*)

      (* prove remaining subgoals *)

      2: intro s_neq_y.
      2: assert (s1: subs y (Abs s (subs x M N)) L = Abs s (subs y (subs x M N) L)).
      2:   apply (subs_abs_neq y s (subs x M N) L).
      2:   auto.
      2: rewrite s1.
      2: assert (s2: subs x (Abs s (subs y M L)) (subs y N L) = Abs s (subs x (subs y M L) (subs y N L))).
      2:   apply (subs_abs_neq x s (subs y M L) (subs y N L)).
      2:   auto.
      2: rewrite s2.
      2: rewrite IHM.
      2: trivial.

      2: unfold subs; fold subs.
      2: rewrite IHM1; rewrite IHM2.
      2: trivial. (* this finishes the proof *)

(* the rest of this script is commented. it was just some experiments with Coq *)

(*
case (string_dec s x).
        intros s_eq_x' s_eq_y.
        apply sym_eq in s_eq_x.
        assert (x_eq_y: x = y).
          apply (trans_eq s_eq_x s_eq_y).
        contradiction.
        contradiction.
    unfold subs at 1; fold subs.
    case (string_dec s y).
      contradiction.
    unfold subs at 2; fold subs.
    case (string_dec s x).
      trivial.
    contradiction.

    intro s_neq_x.
    unfold subs at 4; fold subs.
    case (string_dec s y).
      intro s_eq_y.
      unfold subs at 3; fold subs.
      case (string_dec s x).
        contradiction.
      intro.
      unfold subs at 1; fold subs.
      apply subs_abs.
      unfold subs at 3; fold subs.
    case (string_dec s y).
      2: contradiction.
    unfold subs at 2; fold subs.
    case (string_dec s x).
    contradiction.




    apply IHM.
          (*following experimental*)
          4: intro s_neq_x.
          4: case (string_dec s y).
          4: intro s_eq_y.
          Show 6.
          Require Import DecidableType. (*?*)
          eq_sym s_eq_x; eq_trans s_eq_x s_eq_y

          .
        absurd x_neq_y.
    auto.
    unfold subs; fold subs.
*)
Qed.