From Undecidability.FOL.Util Require Import Syntax Syntax_facts FullTarski FullTarski_facts FullDeduction_facts FullDeduction.
Require Import Undecidability.FOL.PA.
Require Import Lia List Vector.
Import Vector.VectorNotations.

Lemma bounded_S_exists N phi : bounded (S N) phi <-> bounded N ( phi).
Proof.
  split; intros H.
  - now constructor.
  - inversion H. apply inj_pair2_eq_dec' in H4 as ->; trivial.
    unfold Dec.dec. decide equality.
Qed.

Lemma bounded_S_forall N phi : bounded (S N) phi <-> bounded N ( phi).
Proof.
  split; intros H.
  - now constructor.
  - inversion H. apply inj_pair2_eq_dec' in H4 as ->; trivial.
    unfold Dec.dec. decide equality.
Qed.

Section ND.

  Variable p : peirce.

  Fixpoint iter {X: Type} f n (x : X) :=
    match n with
      0 => x
    | S m => f (iter f m x)
    end.

  Fact iter_switch {X} f n x : f (@iter X f n x) = iter f n (f x).
  Proof. induction n; cbn; now try rewrite IHn. Qed.


  Lemma subst_up_var k x sigma : x < k -> (var x)`[iter up k sigma] = var x.
  Proof.
    induction k in x, sigma |-*.
    - now intros ?%PeanoNat.Nat.nlt_0_r.
    - intros H.
      destruct (Compare_dec.lt_eq_lt_dec x k) as [[| <-]|].
      + cbn [iter]. rewrite iter_switch. now apply IHk.
      + destruct x. reflexivity.
        change (iter _ _ _) with (up (iter up (S x) sigma)).
        change (var (S x)) with ((var x)`[]).
        rewrite up_term, IHk. reflexivity. constructor.
      + lia.
  Qed.


  Lemma subst_bounded_term t sigma k : bounded_t k t -> t`[iter up k sigma] = t.
  Proof.
    induction 1.
    - now apply subst_up_var.
    - cbn. f_equal.
      rewrite <-(Vector.map_id _ _ v) at 2.
      apply Vector.map_ext_in. auto.
  Qed.

  Lemma subst_bounded k phi sigma : bounded k phi -> phi[iter up k sigma] = phi.
  Proof.
    induction 1 in sigma |-*; cbn.
    - f_equal.
      rewrite <-(Vector.map_id _ _ v) at 2.
      apply Vector.map_ext_in.
      intros t Ht. apply subst_bounded_term. auto.
    - now rewrite IHbounded1, IHbounded2.
    - f_equal.
      change (up _) with (iter up (S n) sigma).
      apply IHbounded.
    - reflexivity.
  Qed.

  Definition exist_times n (phi : form) := iter (fun psi => psi) n phi.
  Definition forall_times n (phi : form) := iter (fun psi => psi) n phi.

  Lemma up_decompose sigma phi : phi[up (S >> sigma)][(sigma 0)..] = phi[sigma].
  Proof.
    rewrite subst_comp. apply subst_ext.
    intros [].
    - reflexivity.
    - apply subst_term_shift.
  Qed.


  Lemma subst_exist_prv {sigma N Gamma} phi :
    Gamma phi[sigma] -> bounded N phi -> Gamma exist_times N phi.
  Proof.
    induction N in phi, sigma |-*; intros; cbn.
    - erewrite <-(subst_bounded 0); eassumption.
    - rewrite iter_switch. eapply (IHN (S >> sigma)).
      cbn. eapply (ExI (sigma 0)).
      now rewrite up_decompose.
      now apply bounded_S_exists.
  Qed.


  Lemma subst_forall_prv phi {N Gamma} :
    Gamma (iter (fun psi => psi) N phi) -> bounded N phi -> forall sigma, Gamma phi[sigma].
  Proof.
    induction N in phi |-*; intros ?? sigma; cbn in *.
    - change sigma with (iter up 0 sigma).
      now rewrite (subst_bounded 0).
    - specialize (IHN ( phi) ).
      rewrite <-up_decompose.
      apply AllE. apply IHN.
      now rewrite <-iter_switch.
      now apply bounded_S_forall.
  Qed.

End ND.

Section SEM.

  Context {D : Type}.
  Context {I : interp D}.


  Lemma bounded_eval_t n t sigma tau :
    (forall k, n > k -> sigma k = tau k) -> bounded_t n t -> eval sigma t = eval tau t.
  Proof.
    intros H. induction 1; cbn; auto.
    f_equal. now apply Vector.map_ext_in.
  Qed.


  Lemma bound_ext N phi rho sigma :
    bounded N phi -> (forall n, n < N -> rho n = sigma n) -> (rho phi <-> sigma phi).
  Proof.
    induction 1 in sigma, rho |- *; cbn; intros HN; try tauto.
    - enough (map (eval rho) v = map (eval sigma) v) as E. now setoid_rewrite E.
      apply Vector.map_ext_in. intros t Ht.
      eapply bounded_eval_t; try apply HN. now apply H.
    - destruct binop; now rewrite (IHbounded1 rho sigma), (IHbounded2 rho sigma).
    - destruct quantop.
      + split; intros Hd d; eapply IHbounded.
        all : try apply (Hd d); intros [] Hk; cbn; auto.
        symmetry. all: apply HN; lia.
      + split; intros [d Hd]; exists d; eapply IHbounded.
        all : try apply Hd; intros [] Hk; cbn; auto.
        symmetry. all: apply HN; lia.
  Qed.

  Corollary sat_closed rho sigma phi :
    bounded 0 phi -> rho phi <-> sigma phi.
  Proof.
    intros H. eapply bound_ext. apply H. lia.
  Qed.


  Lemma subst_exist_sat rho phi N :
    rho phi -> bounded N phi -> forall rho, rho (exist_times N phi).
  Proof.
    induction N in phi, rho |-*; intros.
    - cbn. eapply sat_closed; eassumption.
    - cbn -[sat]. rewrite iter_switch. apply (IHN (S >> rho)).
      exists (rho 0). eapply sat_ext. 2: apply H.
      now intros [].
      now apply bounded_S_exists.
  Qed.

  Fact subst_exist_sat2 N : forall rho phi, rho (exist_times N phi) -> (exists sigma, sigma phi).
  Proof.
    induction N.
    - eauto.
    - intros rho phi [? H]. now apply IHN in H.
  Qed.

End SEM.

Section FA_prv.

  Variable p : peirce.

  Variable Gamma : list form.
  Variable G : incl FAeq Gamma.


  Fixpoint join {X n} (v : t X n) (rho : nat -> X) :=
    match v with
    | Vector.nil _ => rho
    | Vector.cons _ x n w => join w (x.:rho)
    end.

  Local Notation "v '∗' rho" := (join v rho) (at level 20).

  Arguments Weak {_ _ _ _}, _.


  Lemma reflexivity t : Gamma (t == t).
  Proof.
    apply (Weak FAeq).

    pose (sigma := [t] var ).
    change (FAeq _) with (FAeq ($0 == $0)[sigma]).

    eapply (@subst_forall_prv _ _ 1).
    apply Ctx. all : firstorder. constructor.
    repeat solve_bounds.
  Qed.


  Lemma symmetry x y : Gamma (x == y) -> Gamma (y == x).
  Proof.
    apply IE. apply (Weak FAeq).

    pose (sigma := [x ; y] var ).
    change (FAeq _) with (FAeq ($1 == $0 ~> $0 == $1)[sigma]).

    apply (@subst_forall_prv _ _ 2).
    apply Ctx. all : firstorder.
    repeat solve_bounds.
  Qed.


  Lemma transitivity x y z :
    Gamma (x == y) -> Gamma (y == z) -> Gamma (x == z).
  Proof.
    intros H. apply IE. revert H; apply IE.
    apply Weak with FAeq.

    pose (sigma := [x ; y ; z] var).
    change (FAeq _) with (FAeq ($2 == $1 ~> $1 == $0 ~> $2 == $0)[sigma]).

    apply (@subst_forall_prv _ _ 3).
    apply Ctx. all : try firstorder.
    repeat solve_bounds.
  Qed.

  Lemma eq_succ x y : Gamma (x == y) -> Gamma (σ x == σ y).
  Proof.
    apply IE. apply Weak with FAeq.

    pose (sigma := [y ; x] var ).
    change (FAeq _) with (FAeq ($0 == $1 ~> σ $0 == σ $1)[sigma]).

    apply (@subst_forall_prv _ _ 2).
    apply Ctx. all : firstorder.
    repeat solve_bounds.
  Qed.


  Lemma eq_add {x1 y1 x2 y2} :
    Gamma (x1 == x2) -> Gamma (y1 == y2) -> Gamma (x1 y1 == x2 y2).
  Proof.
    intros H; apply IE. revert H; apply IE.
    apply Weak with FAeq.

    pose (sigma := [y2 ; y1 ; x2 ; x1] var).
    change (FAeq _) with (FAeq ($0 == $1 ~> $2 == $3 ~> $0 $2 == $1 $3)[sigma]).

    apply (@subst_forall_prv _ _ 4).
    apply Ctx. all: firstorder.
    repeat solve_bounds.
  Qed.

  Lemma eq_mult {x1 y1 x2 y2} :
    Gamma (x1 == x2) -> Gamma (y1 == y2) -> Gamma (x1 y1 == x2 y2).
  Proof.
    intros H; apply IE. revert H; apply IE.
    apply Weak with FAeq.

    pose (sigma := [y2 ; y1 ; x2 ; x1] var).
    change (FAeq _) with (FAeq ($0 == $1 ~> $2 == $3 ~> $0 $2 == $1 $3)[sigma]).

    apply (@subst_forall_prv _ _ 4).
    apply Ctx. all: firstorder.
    repeat solve_bounds.
  Qed.


  Lemma Add_rec x y : Gamma ( (σ x) y == σ (x y) ).
  Proof.
    apply Weak with FAeq.

    pose (sigma := [y ; x] var).
    change (FAeq _) with (FAeq (σ $0 $1 == σ ($0 $1))[sigma]).

    apply (@subst_forall_prv _ _ 2).
    apply Ctx. all : firstorder.
    repeat solve_bounds.
  Qed.

  Fixpoint num n := match n with
                       O => zero
                     | S x => σ (num x)
                     end.

  Lemma num_add_homomorphism x y : Gamma ( num x num y == num (x + y) ).
  Proof.
    induction x; cbn.
    - apply (@AllE _ _ _ _ _ _ (zero $0 == $0) ).
      apply Weak with FAeq.
      apply Ctx;firstorder.
      assumption.
    - eapply transitivity.
      apply Add_rec.
      now apply eq_succ.
  Qed.

  Lemma Mult_rec x y : Gamma ( (σ x) y == y (x y) ).
  Proof.
    apply Weak with FAeq.

    pose (sigma := [x ; y] var).
    change (FAeq _) with (FAeq ((σ $1) $0 == $0 ($1 $0))[sigma]).

    eapply (@subst_forall_prv _ _ 2).
    apply Ctx. all : firstorder.
    repeat solve_bounds.
  Qed.


  Lemma num_mult_homomorphism (x y : nat) : Gamma ( num x num y == num (x * y) ).
  Proof.
    induction x; cbn.
    - apply (@AllE _ _ _ _ _ _ (zero $0 == zero)).
      apply Weak with FAeq. apply Ctx; firstorder.
      assumption.
    - eapply transitivity.
      apply Mult_rec.
      eapply transitivity.
      2: apply num_add_homomorphism.
      apply eq_add. apply reflexivity. apply IHx.
  Qed.

End FA_prv.

Notation "x 'i=' y" := (i_atom (P:=Eq) [x ; y]) (at level 30) : PA_Notation.
Notation "'iO'" := (i_func (Σ_funcs:=PA_funcs_signature) (f:=Zero) []) (at level 2) : PA_Notation.
Notation "'iσ' d" := (i_func (f:=Succ) [d]) (at level 37) : PA_Notation.
Notation "x 'i⊕' y" := (i_func (f:=Plus) [x ; y]) (at level 39) : PA_Notation.
Notation "x 'i⊗' y" := (i_func (f:=Mult) [x ; y]) (at level 38) : PA_Notation.


Section FA_models.

  Variable D : Type.
  Variable I : interp D.

  Hypothesis ext_model : extensional I.
  Hypothesis FA_model : forall ax rho, List.In ax FA -> rho ax.

  Fixpoint k := match k with
                   | O => iO
                   | S n => iσ ( n)
                   end.


  Fact eval_num sigma n : eval sigma (num n) = n.
  Proof.
    induction n.
    - reflexivity.
    - cbn. now rewrite IHn.
  Qed.

  Lemma add_zero : forall d : D, iO i d = d.
  Proof.
    intros d.
    assert (List.In ax_add_zero FA) as H by firstorder.
    specialize (FA_model ax_add_zero (d.:(fun _ => iO)) H).
    cbn in FA_model. now apply ext_model.
  Qed.

  Lemma add_rec : forall n d : D, iσ n i d = iσ (n i d).
  Proof.
    intros n d.
    assert (List.In ax_add_rec FA) as H by firstorder.
    specialize (FA_model ax_add_rec (d.:(fun _ => iO)) H).
    cbn in FA_model. now apply ext_model.
  Qed.

  Lemma mult_zero : forall d : D, iO i d = iO.
  Proof.
    intros d.
    assert (List.In ax_mult_zero FA) as H by firstorder.
    specialize (FA_model ax_mult_zero (d.:(fun _ => iO)) H).
    cbn in FA_model. now apply ext_model.
  Qed.

  Lemma mult_rec : forall n d : D, iσ d i n = n i d i n.
  Proof.
    intros n d.
    assert (List.In ax_mult_rec FA) as H by firstorder.
    specialize (FA_model ax_mult_rec (d.:(fun _ => iO)) H).
    cbn in FA_model. now apply ext_model.
  Qed.

  Corollary add_hom x y : (x + y) = x i y.
  Proof.
    induction x.
    - now rewrite add_zero.
    - change (iσ (x + y) = iσ x i y).
      now rewrite add_rec, IHx.
  Qed.

  Corollary add_nat_to_model : forall x y z, x + y = z -> ( x i y = z).
  Proof.
    intros x y z H. now rewrite <- add_hom, H.
  Qed.

  Corollary mult_hom x y : (x * y) = x i y.
  Proof.
    induction x.
    - now rewrite mult_zero.
    - change ( (y + x * y) = (iσ x) i y ).
      now rewrite add_hom, IHx, mult_rec.
  Qed.

  Corollary mult_nat_to_model : forall z x y, x * y = z -> ( x i y = z).
  Proof.
    intros x y z H. now rewrite <- mult_hom, H.
  Qed.


End FA_models.

Arguments {_ _} _.

The standard model


Section StdModel.

  Definition interp_nat : interp nat.
  Proof.
    split.
    - destruct f; intros v.
      + exact 0.
      + exact (S (Vector.hd v) ).
      + exact (Vector.hd v + Vector.hd (Vector.tl v) ).
      + exact (Vector.hd v * Vector.hd (Vector.tl v) ).
    - destruct P. intros v.
      exact (Vector.hd v = Vector.hd (Vector.tl v) ).
  Defined.


  Fact nat_extensional : extensional interp_nat.
  Proof.
    now intros x y.
  Qed.


  Lemma nat_is_FA_model : forall rho phi, List.In phi FAeq -> sat interp_nat rho phi.
  Proof.
    intros rho phi. intros H.
    repeat (destruct H as [<- | H]; auto).
    all: cbn; try congruence.
  Qed.

  Lemma nat_is_Q_model : forall rho phi, List.In phi Qeq -> sat interp_nat rho phi.
  Proof.
    intros rho phi. intros H.
    repeat (destruct H as [<- | H]; auto).
    all: cbn; try congruence.
    induction d. now left.
    right. destruct IHd.
    exists 0. congruence.
    exists d. reflexivity.
  Qed.


  Fact nat_eval_num (sigma : env nat) n : @eval _ _ _ interp_nat sigma (num n) = n.
  Proof.
    induction n.
    - reflexivity.
    - cbn. now rewrite IHn.
  Qed.

  Fact nat_induction phi : forall rho, sat interp_nat rho (ax_induction phi).
  Proof.
    intros rho H0 IH d. induction d; cbn in *.
    rewrite <-sat_single in H0. apply H0.
    apply IH in IHd. rewrite sat_comp in IHd.
    revert IHd. apply sat_ext. intros []; reflexivity.
  Qed.

  Fact nat_is_PAeq_model : forall ax rho, PAeq ax -> sat interp_nat rho ax.
  Proof.
    intros rho psi [].
    now apply nat_is_FA_model.
    all: cbn; try congruence.
    apply nat_induction.
 Qed.

  Fact nat_is_PA_model : forall ax rho, PA ax -> sat interp_nat rho ax.
  Proof.
    intros rho psi [].
    repeat (destruct H as [<- | H]; auto).
    all: cbn; try congruence.
    apply nat_induction.
  Qed.


End StdModel.