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.
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.
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.
- change (iσ (x + y) = iσ x i y).
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 ).
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.