(* * Conservativity *)

From Undecidability.FOL Require Import Util.FullTarski_facts Util.Syntax_facts Util.FullDeduction_facts.
From Undecidability.FOL Require Import ZF Reductions.PCPb_to_ZF Reductions.PCPb_to_minZF minZF Reductions.PCPb_to_ZFeq.
From Undecidability Require Import Shared.ListAutomation.
Import ListAutomationNotations.
Local Set Implicit Arguments.
Local Unset Strict Implicit.

Require Import Equations.Equations.
Require Import Morphisms.

Local Notation vec := Vector.t.

(* ** Semantics *)

Section Model.

  Open Scope sem.

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

  Hypothesis M_ZF : rho, ZFeq'.

  Instance min_model : interp sig_empty _ V.
  Proof.
    split.
    - intros [].
    - now apply i_atom.
  Defined.


  Lemma min_embed_eval (rho : V) (t : term') :
    eval (embed_t t) = eval t.
  Proof.
    destruct t as [|[]]. reflexivity.
  Qed.


  Lemma min_embed (rho : V) (phi : form') :
    sat I (embed ) sat min_model .
  Proof.
    induction in |- *; try destruct ; try destruct q; cbn.
    1,3-7: firstorder. erewrite Vector.map_map, Vector.map_ext.
    reflexivity. apply min_embed_eval.
  Qed.


  Lemma embed_subst_t (sigma : term') (t : term') :
    embed_t t`[] = (embed_t t)`[ >> embed_t].
  Proof.
    induction t; cbn; trivial. destruct F.
  Qed.


  Lemma embed_subst (sigma : term') (phi : form') :
    embed [] = (embed )[ >> embed_t].
  Proof.
    induction in |- *; cbn; trivial.
    - f_equal. erewrite !Vector.map_map, Vector.map_ext. reflexivity. apply embed_subst_t.
    - firstorder congruence.
    - rewrite IHphi. f_equal. apply subst_ext. intros []; cbn; trivial.
      unfold funcomp. cbn. unfold funcomp. now destruct ( n) as [x|[]].
  Qed.


  Lemma embed_sshift n (phi : form') :
    embed [sshift n] = (embed )[sshift n].
  Proof.
    rewrite embed_subst. apply subst_ext. now intros [].
  Qed.


  Lemma sat_sshift1 (rho : V) x y (phi : form) :
    (y .: x .: ) [sshift 1] (y .: ) .
  Proof.
    erewrite sat_comp, sat_ext. reflexivity. now intros [].
  Qed.


  Lemma sat_sshift2 (rho : V) x y z (phi : form) :
    (z .: y .: x .: ) [sshift 2] (z .: ) .
  Proof.
    erewrite sat_comp, sat_ext. reflexivity. now intros [].
  Qed.


  Lemma inductive_sat (rho : V) x :
    (x .: ) is_inductive $0 M_inductive x.
  Proof.
    cbn. split.
    - destruct H as [[y Hy] _]. enough (H : y).
      { eapply set_equiv_elem; eauto. now apply set_equiv_equiv. apply Hy. }
      apply M_ext; trivial; intros z Hz; exfalso; intuition. now apply M_eset in Hz.
    - intros y [z Hz] % H. enough (Hx : σ y z).
      { eapply set_equiv_elem; eauto. now apply set_equiv_equiv. apply Hz. }
      apply M_ext; trivial.
      + intros a Ha % sigma_el; trivial. now apply Hz.
      + intros a Ha % Hz. now apply sigma_el.
  Qed.


  Lemma inductive_sat_om (rho : V) :
    (ω .: ) is_inductive $0.
  Proof.
    cbn. split.
    - exists . split; try apply M_eset; trivial. now apply M_om1.
    - intros d Hd. exists (σ d). split; try now apply M_om1. intros d'. now apply sigma_el.
  Qed.


  Instance set_equiv_equiv' :
    Equivalence set_equiv.
  Proof.
    now apply set_equiv_equiv.
  Qed.


  Instance set_equiv_elem' :
    Proper (set_equiv set_equiv iff) set_elem.
  Proof.
    now apply set_equiv_elem.
  Qed.


  Instance set_equiv_sub' :
    Proper (set_equiv set_equiv iff) set_sub.
  Proof.
    now apply set_equiv_sub.
  Qed.


  Instance equiv_union' :
    Proper (set_equiv set_equiv) union.
  Proof.
    now apply equiv_union.
  Qed.


  Instance equiv_power' :
    Proper (set_equiv set_equiv) power.
  Proof.
    now apply equiv_power.
  Qed.


  Lemma rm_const_tm_sat (rho : V) (t : term) x :
    (x .: ) embed (rm_const_tm t) set_equiv x (eval t).
  Proof.
    induction t in x |- *; try destruct F; cbn; split;
    try rewrite (vec_inv1 v); try rewrite (vec_inv2 v); cbn.
    - tauto.
    - tauto.
    - rewrite (vec_nil_eq (Vector.map (eval ) v)).
      intros H. apply M_ext; trivial; intros y Hy; exfalso; intuition.
      now apply M_eset in Hy.
    - rewrite (vec_nil_eq (Vector.map (eval ) v)).
      change (set_equiv x d : V, set_elem d x False).
      intros H d. rewrite H. now apply M_eset.
    - intros (y & Hy & z & Hz & H).
      rewrite embed_sshift, sat_sshift1, IH in Hy; try apply in_hd.
      rewrite embed_sshift, sat_sshift2, IH in Hz; try apply in_hd_tl.
      apply M_ext; trivial.
      + intros a Ha % H. apply M_pair; trivial.
        rewrite Hy, Hz. tauto.
      + intros a Ha % M_pair; trivial. apply H.
        rewrite Hy, Hz in Ha. tauto.
    - exists (eval (Vector.hd v)).
      rewrite embed_sshift, sat_sshift1, IH; try apply in_hd. split; try reflexivity.
      exists (eval (Vector.hd (Vector.tl v))).
      rewrite embed_sshift, sat_sshift2, IH; try apply in_hd_tl. split; try reflexivity.
      change ( d, (set_elem d x d eval (Vector.hd v) d eval (Vector.hd (Vector.tl v)))
              (d eval (Vector.hd v) d eval (Vector.hd (Vector.tl v)) set_elem d x)).
      intros d. rewrite H. now apply M_pair.
    - intros (y & Hy & H). rewrite embed_sshift, sat_sshift1, IH in Hy; try apply in_hd.
      change (set_equiv x (union (eval (Vector.hd v)))). rewrite Hy. apply M_ext; trivial.
      + intros z Hz % H. now apply M_union.
      + intros z Hz % M_union; trivial. now apply H.
    - exists (eval (Vector.hd v)). rewrite embed_sshift, sat_sshift1, IH; try apply in_hd. split; try reflexivity.
      change ( d, (set_elem d x d0 : V, eval (Vector.hd v) d )
              (( d0 : V, eval (Vector.hd v) d ) set_elem d x)).
      intros d. rewrite H. now apply M_union.
    - intros (y & Hy & H). rewrite embed_sshift, sat_sshift1, IH in Hy; try apply in_hd.
      change (set_equiv x (power (eval (Vector.hd v)))). rewrite Hy. apply M_ext; trivial.
      + intros z Hz. apply M_power; trivial. unfold set_sub. now apply H.
      + intros z Hz. now apply H, M_power.
    - exists (eval (Vector.hd v)).
      rewrite embed_sshift, sat_sshift1, IH; try apply in_hd. split; try reflexivity.
      change ( d, (set_elem d x d eval (Vector.hd v)) (d eval (Vector.hd v) set_elem d x)).
      intros d. rewrite H. now apply M_power.
    - rewrite (vec_nil_eq (Vector.map (eval ) v)). intros [ ]. apply M_ext; trivial.
      + unfold set_sub. apply . apply (inductive_sat_om ).
      + unfold set_sub. apply M_om2; trivial. apply inductive_sat with . apply .
    - rewrite (vec_nil_eq (Vector.map (eval ) v)). split.
      + change (( d : V, ( d0 : V, d False) set_elem d x) ( d : V, set_elem d x
             d0 : V, ( d1 : V, ( d d) ( d d )) set_elem x)).
        setoid_rewrite H. apply (inductive_sat_om ).
      + intros d Hd. change (set_sub x d). rewrite H. unfold set_sub.
        apply M_om2; trivial. apply inductive_sat with . apply Hd.
  Qed.


  Lemma rm_const_sat (rho : V) (phi : form) :
     embed (rm_const_fm ).
  Proof.
    induction in |- *; try destruct P; try destruct ; try destruct q; cbn. 1,4-6: intuition.
    - rewrite (vec_inv2 t). cbn. split.
      + intros H. exists (eval (Vector.hd t)). rewrite rm_const_tm_sat. split; try reflexivity.
        exists (eval (Vector.hd (Vector.tl t))). now rewrite embed_sshift, sat_sshift1, rm_const_tm_sat.
      + intros (x & Hx & y & Hy & H). apply rm_const_tm_sat in Hx.
        change (set_elem (eval (Vector.hd t)) (eval (Vector.hd (Vector.tl t)))).
        rewrite embed_sshift, sat_sshift1, rm_const_tm_sat in Hy. now rewrite Hx, Hy.
    - rewrite (vec_inv2 t). cbn. split.
      + intros H. exists (eval (Vector.hd t)). rewrite rm_const_tm_sat. split; try reflexivity.
        exists (eval (Vector.hd (Vector.tl t))). rewrite embed_sshift, sat_sshift1, rm_const_tm_sat.
        split; trivial. reflexivity.
      + intros (x & Hx & y & Hy & H). apply rm_const_tm_sat in Hx.
        change (set_equiv (eval (Vector.hd t)) (eval (Vector.hd (Vector.tl t)))).
        rewrite embed_sshift, sat_sshift1, rm_const_tm_sat in Hy. now rewrite Hx, Hy.
    - split; intros; intuition.
    - firstorder eauto.
  Qed.


  Theorem min_correct (rho : V) (phi : form) :
    sat I sat min_model (rm_const_fm ).
  Proof.
    rewrite min_embed. apply rm_const_sat.
  Qed.


  Lemma min_axioms' (rho : V) :
     minZFeq'.
  Proof.
    intros A [|[|[|[|[|[|[|[|[|[|[]]]]]]]]]]]; cbn.
    - now apply set_equiv_equiv.
    - now apply set_equiv_equiv.
    - now apply set_equiv_equiv.
    - intros x x' y y' Hx Hy. now apply set_equiv_elem.
    - intros x y . now apply M_ext.
    - exists . apply (@M_ZF ax_eset). firstorder.
    - intros x y. exists ({x; y}). apply (@M_ZF ax_pair). firstorder.
    - intros x. exists ( x). apply (@M_ZF ax_union). firstorder.
    - intros x. exists (PP x). apply (@M_ZF ax_power). firstorder.
    - exists ω. split. split.
      + exists . split. apply (@M_ZF ax_eset). firstorder. apply (@M_ZF ax_om1). firstorder.
      + intros x Hx. exists (σ x). split. 2: apply (@M_ZF ax_om1); firstorder.
        intros y. now apply sigma_el.
      + intros x [ ]. apply (@M_ZF ax_om2); cbn. auto 12. split.
        * destruct as (e & & ). change (set_elem x).
          enough (set_equiv e) as by assumption.
          apply M_ext; trivial. all: intros y Hy; exfalso; try now apply in Hy.
          apply (@M_ZF ax_eset) in Hy; trivial. unfold ZFeq', ZF'. auto 8.
        * intros d (s & & ) % . change (set_elem (σ d) x).
          enough (set_equiv (σ d) s) as by assumption.
          apply M_ext; trivial. all: intros y; rewrite sigma_el; trivial; apply .
  Qed.


End Model.