(** * FOL Reductions *)

Require Export FOL.PCP Deduction.

(** ** Validity *)

Section validity.

  Notation u := 0. Notation v := 1.
  Context {b : logic}.
  Variable R : BSRS.

  Definition prep (x : string bool) (t : term) : term := fold_right t_f t x.
  Definition iprep domain eta {I : interp domain eta} (x : list bool) (y : domain) := fold_right i_f y x.
  Definition enc s := (prep s t_e).

  Definition F1 := map (fun '(x,y) => Pr (enc x) (enc y)) R.
  Definition F2 := map (fun '(x, y) => ∀ u; ∀ v; Pr u v --> Pr (prep x u) (prep y v)) R.
  Definition F3 := (∀ u; Pr u u --> Q).

  Definition F : form b := F1 ==> F2 ==> F3 --> Q.

  Lemma enc_vars x :
    vars_t (enc x) = [].
  Proof.
(* Goal: @eq (list nat) (vars_t (enc x)) (@nil nat) *)
    induction x; trivial.
  Qed.

  Lemma prep_subst y t1 x t :
    subst_t y t1 (prep x t) = prep x (subst_t y t1 t).
  Proof.
(* Goal: @eq term (subst_t y t1 (prep x t)) (prep x (subst_t y t1 t)) *)
    induction x; cbn; f_equal; eauto.
  Qed.

  Lemma prep_vars x t :
    vars_t (prep x t) = vars_t t.
  Proof.
(* Goal: @eq (list nat) (vars_t (prep x t)) (vars_t t) *)
    induction x; cbn; eauto.
  Qed.

  Lemma iprep_eval domain eta (I : interp domain eta) rho x s :
    eval rho (prep x s) = iprep x (eval rho s).
  Proof.
(* Goal: @eq domain (@eval domain eta I rho (prep x s)) (@iprep domain eta I x (@eval domain eta I rho s)) *)
    induction x; cbn; now do 2 f_equal.
  Qed.

  Lemma iprep_app domain eta (I : interp domain eta) x y d :
    iprep (x ++ y) d = iprep x (iprep y d).
  Proof.
(* Goal: @eq domain (@iprep domain eta I (@app bool x y) d) (@iprep domain eta I x (@iprep domain eta I y d)) *)
    unfold iprep. now rewrite fold_right_app.
  Qed.
  
  Global Instance IB : interp (string bool) (fun _ => []) :=
    {|
      i_f b s := b :: s ;
      i_e := nil;
      i_P u v := derivable R u v ;
      i_Q := BPCP' R
    |}.

  Lemma IB_prep rho s t :
    eval rho (prep s t) = s ++ eval rho t.
  Proof.
(* Goal: @eq (list bool) (@eval (list bool) (fun _ : nat => @nil bool) IB rho (prep s t)) (@app bool s (@eval (list bool) (fun _ : nat => @nil bool) IB rho t)) *)
    induction s; cbn; trivial.
(* Goal: @eq (list bool) (@cons bool a (@eval (list bool) (fun _ : nat => @nil bool) IB rho (@fold_right term bool t_f t s))) (@cons bool a (@app bool s (@eval (list bool) (fun _ : nat => @nil bool) IB rho t))) *)
    rewrite <- IHs. reflexivity.
  Qed.

  Lemma IB_enc rho s :
    eval rho (enc s) = s.
  Proof.
(* Goal: @eq (string bool) (@eval (string bool) (fun _ : nat => @nil bool) IB rho (enc s)) s *)
    unfold enc. rewrite IB_prep.
(* Goal: @i_P (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB (@eval (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB (@update (option (string bool)) rho O (@None (string bool))) (V O)) (@eval (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB (@update (option (string bool)) rho O (@None (string bool))) (V O)) *)
    cbn. apply app_nil_r.
  Qed.

  Lemma IB_drv rho t1 t2 :
    rho ⊨ (Pr t1 t2) <-> derivable R (eval rho t1) (eval rho t2).
  Proof.
(* Goal: iff (@derivable bool R u v) (@derivable bool R u v) *)
    cbn. reflexivity.
  Qed.

  Lemma IB_F1 rho :
    rho ⊫ F1.
  Proof.
(* Goal: forall (psi : form b) (_ : @In (form b) psi F1), @sat (string bool) (fun _ : nat => @nil bool) IB b rho psi *)
    unfold F1. 
(* Goal: forall (psi : form b) (_ : @In (form b) psi (@map (prod (string bool) (string bool)) (form b) (fun '(pair x y) => @Pr b (enc x) (enc y)) R)), @sat (string bool) (fun _ : nat => @nil bool) IB b rho psi *)
    intros ? ([x y] & <- & ?) % in_map_iff.
(* Goal: @i_P (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB (@eval (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB (@update (option (string bool)) rho O (@None (string bool))) (V O)) (@eval (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB (@update (option (string bool)) rho O (@None (string bool))) (V O)) *)
    cbn. econstructor. now rewrite !IB_enc.
  Qed.

  Lemma IB_F2 rho :
    rho ⊫ F2.
  Proof.
(* Goal: @i_P (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB (@eval (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB (@update (option (string bool)) rho O (@None (string bool))) (V O)) (@eval (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB (@update (option (string bool)) rho O (@None (string bool))) (V O)) *)
    unfold F2. intros ? ([x y] & <- & ?) % in_map_iff u v ?. cbn.
(* Goal: @derivable bool R (@eval (string bool) (fun _ : nat => @nil bool) IB (@update (string bool) (@update (string bool) rho O u) (S O) v) (prep x (V O))) (@eval (string bool) (fun _ : nat => @nil bool) IB (@update (string bool) (@update (string bool) rho O u) (S O) v) (prep y (V (S O)))) *)
    rewrite !IB_prep. cbn in *. eauto using derivable.
  Qed.

  Lemma IB_F3 rho :
    rho ⊨ F3.
  Proof.
(* Goal: @i_P (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB (@eval (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB (@update (option (string bool)) rho O (@None (string bool))) (V O)) (@eval (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB (@update (option (string bool)) rho O (@None (string bool))) (V O)) *)
    cbn. apply cBPCP.
  Qed.

  Lemma IB_F rho :
    rho ⊨ F -> BPCP' R.
  Proof.
(* Goal: @sat (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB full rho (@Impl full (@All full O (@Impl full (@Pr full (V O) (V O)) Fal)) Fal) *)
    intros H. unfold F in H. rewrite !impl_sat in H. eapply H.
    - eapply IB_F1.
    - eapply IB_F2.
    - apply IB_F3.
  Qed.

  Lemma drv_val domain eta (I : interp domain eta) rho u v :
    derivable R u v -> rho ⊨ (F1 ==> F2 ==> Pr (enc u) (enc v)).
  Proof.
(* Goal: forall _ : @derivable bool R u v, @sat domain eta I b rho (@impl b F1 (@impl b F2 (@Pr b (enc u) (enc v)))) *)
    rewrite !impl_sat. intros. induction H.
    - eapply H0. eapply in_map_iff. exists (x/y). eauto.
    - eapply (H1 (∀ 0; ∀ 1; Pr 0 1 --> Pr (prep x 0) (prep y 1))) in IHderivable.
(* Goal: @i_P (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB (@eval (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB (@update (option (string bool)) rho O (@None (string bool))) (V O)) (@eval (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB (@update (option (string bool)) rho O (@None (string bool))) (V O)) *)
      + cbn. unfold enc in *. rewrite !iprep_eval in *. cbn in IHderivable.
        rewrite <- !iprep_app in IHderivable. eapply IHderivable.
(* Goal: @In (form b) (@All b O (@All b (S O) (@Impl b (@Pr b (V O) (V (S O))) (@Pr b (prep x (V O)) (prep y (V (S O))))))) F2 *)
      + eapply in_map_iff. exists (x/y). eauto.
  Qed.

  Theorem BPCP_valid :
    BPCP R <-> valid F.
  Proof.
(* Goal: iff (not (BPCP R)) (@satis full (@Impl full (@F full R) Fal)) *)
    rewrite BPCP_BPCP'. split.
    - intros [u H] D eta I rho.
(* Goal: @derivable bool R (@app bool x (@eval (list bool) (fun _ : nat => @nil bool) IB (@update (string bool) (@update (string bool) rho O u) (S O) v) (V O))) (@app bool y (@eval (list bool) (fun _ : nat => @nil bool) IB (@update (string bool) (@update (string bool) rho O u) (S O) v) (V (S O)))) *)
      eapply (@drv_val _ _ I) in H. unfold F. cbn in *.
(* Goal: @derivable bool R (@app bool x (@eval (list bool) (fun _ : nat => @nil bool) IB (@update (string bool) (@update (string bool) rho O u) (S O) v) (V O))) (@app bool y (@eval (list bool) (fun _ : nat => @nil bool) IB (@update (string bool) (@update (string bool) rho O u) (S O) v) (V (S O)))) *)
      rewrite !impl_sat in *. cbn in *.
(* Goal: forall (_ : @derivable bool R u v) (_ : forall (psi : form b) (_ : @In (form b) psi F1), @sat domain eta I b rho psi) (_ : forall (psi : form b) (_ : @In (form b) psi F2), @sat domain eta I b rho psi), @sat domain eta I b rho (@Pr b (enc u) (enc v)) *)
      intros. eapply (H2 (eval rho (enc u))). eauto.
(* Goal: @sat (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB full rho (@Impl full (@All full O (@Impl full (@Pr full (V O) (V O)) Fal)) Fal) *)
    - intros H. apply IB_F with (rho := fun _ => nil), H.
  Qed.

  (** ** Provability *)

  Hint Resolve enc_vars.

  Definition ctx_S :=
    F3 :: rev F2 ++ rev F1.

  Lemma drv_prv s u v :
    derivable R u v -> (@prv s b ctx_S (Pr (enc u) (enc v))).
  Proof.
(* Goal: forall _ : @derivable bool R u v, @prv s b ctx_S (@Pr b (enc u) (enc v)) *)
    induction 1.
(* Goal: @prv s b ctx_S (@All b O (@Impl b (@Pr b (V O) (V O)) (@Q b))) *)
(* Goal: @prv s b (@cons (form b) F3 (@app (form b) (@rev (form b) F2) (@rev (form b) F1))) (@Q b) *)
    - econstructor. right. eapply in_app_iff. right.
      rewrite <- in_rev. eapply in_map_iff. exists (x/y). eauto.
    - assert (@prv s b ctx_S (∀ 0; ∀ 1; Pr 0 1 --> Pr (prep x 0) (prep y 1))).
(* Goal: @prv s b ctx_S (@All b O (@Impl b (@Pr b (V O) (V O)) (@Q b))) *)
(* Goal: @prv s b (@cons (form b) F3 (@app (form b) (@rev (form b) F2) (@rev (form b) F1))) (@Q b) *)
      + econstructor. right. eapply in_app_iff. left.
        rewrite <- in_rev. eapply in_map_iff. exists (x/y). eauto.
(* Goal: and (@eq (form b) (@All b O (@All b (S O) (@Impl b (@Pr b (V O) (V (S O))) (@Pr b (prep x (V O)) (prep y (V (S O))))))) (@All b O (@All b (S O) (@Impl b (@Pr b (V O) (V (S O))) (@Pr b (prep x (V O)) (prep y (V (S O)))))))) (@In (prod (string bool) (string bool)) (@pair (string bool) (string bool) x y) R) *)
      + eapply AllE with (t := enc u) in H1; eauto.
(* Goal: @prv s b ctx_S (@Pr b (enc (@app bool x u)) (enc (@app bool y v))) *)
        cbn in H1. rewrite !prep_subst in H1. cbn in H1.
(* Goal: and (@eq (form b) (@All b O (@All b (S O) (@Impl b (@Pr b (V O) (V (S O))) (@Pr b (prep x (V O)) (prep y (V (S O))))))) (@All b O (@All b (S O) (@Impl b (@Pr b (V O) (V (S O))) (@Pr b (prep x (V O)) (prep y (V (S O)))))))) (@In (prod (string bool) (string bool)) (@pair (string bool) (string bool) x y) R) *)
        eapply AllE with (t := enc v) in H1; eauto. cbn in H1.
(* Goal: @prv s b ctx_S (@Pr b (enc (@app bool x u)) (enc (@app bool y v))) *)
        unfold enc in H1. rewrite !prep_subst in H1. cbn in H1.
(* Goal: @prv s b ctx_S (@Pr b (enc (@app bool x u)) (enc (@app bool y v))) *)
        unfold enc, prep in *. rewrite !fold_right_app.
(* Goal: @prv s b ctx_S (@Pr b (@fold_right term bool t_f (@fold_right term bool t_f t_e u) x) (@fold_right term bool t_f (@fold_right term bool t_f t_e v) y)) *)
        eapply (ImpE H1). eassumption.
  Qed.

  Lemma impl_prv s A B phi :
    @prv s b (rev B ++ A) phi -> @ prv s b A (B ==> phi).
  Proof.
(* Goal: forall (_ : @derivable bool R u v) (_ : forall (psi : form b) (_ : @In (form b) psi F1), @sat domain eta I b rho psi) (_ : forall (psi : form b) (_ : @In (form b) psi F2), @sat domain eta I b rho psi), @sat domain eta I b rho (@Pr b (enc u) (enc v)) *)
    revert A; induction B; intros A; cbn; simpl_list; intros.
    - firstorder.
    - eapply ImpI. now eapply IHB.
  Qed.

  Lemma BPCP_prv' s :
    BPCP' R -> @prv s b nil F.
  Proof.
(* Goal: forall _ : BPCP' R, @prv s b (@nil (form b)) F *)
    intros [u H].
(* Goal: @prv s b (@nil (form b)) F *)
    apply drv_prv with (s:=s) in H. unfold F.
(* Goal: @prv s b (@app (form b) (@rev (form b) F2) (@rev (form b) F1)) (@Impl b F3 (@Q b)) *)
    repeat eapply impl_prv. simpl_list. eapply ImpI.
    assert (@prv s b ctx_S (∀ 0; Pr 0 0 --> Q)).
(* Goal: @prv s b ctx_S (@All b O (@Impl b (@Pr b (V O) (V O)) (@Q b))) *)
(* Goal: @prv s b (@cons (form b) F3 (@app (form b) (@rev (form b) F2) (@rev (form b) F1))) (@Q b) *)
    econstructor. now unfold ctx_S. eapply AllE with  (t := enc u) in H0.
(* Goal: @prv s b (@cons (form b) F3 (@app (form b) (@rev (form b) F2) (@rev (form b) F1))) (@Q b) *)
(* Goal: @eq (list nat) (vars_t (enc u)) (@nil nat) *)
    cbn in H0. now eapply (ImpE H0). apply prep_vars.
  Qed.

End validity.

Theorem BPCP_prv R :
  BPCP R <-> nil ⊢M (F R).
Proof.
(* Goal: iff (not (BPCP R)) (@satis full (@Impl full (@F full R) Fal)) *)
  rewrite BPCP_BPCP'. split.
  - apply BPCP_prv'.
  - intros H % soundness. eapply BPCP_BPCP'. now apply (BPCP_valid R).
Qed.

(** ** Satisfiability *)

Lemma valid_satis phi :
  valid phi -> ~ satis (¬ phi).
Proof.
(* Goal: forall _ : @valid full phi, not (@satis full (@Impl full phi Fal)) *)
  intros H1 (D & eta & I & rho & H2).
(* Goal: False *)
  apply H2, (H1 D eta I rho).
Qed.

Theorem BPCP_satis R :
  ~ BPCP R <-> satis (¬ F R).
Proof.
(* Goal: iff (not (BPCP R)) (@satis full (@Impl full (@F full R) Fal)) *)
  rewrite BPCP_BPCP'. split.
(* Goal: @sat (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB full rho (@Impl full (@All full O (@Impl full (@Pr full (V O) (V O)) Fal)) Fal) *)
  - intros H. exists _, (fun _ => nil), (IB R), (fun _ => nil).
(* Goal: @i_P (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB (@eval (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB (@update (option (string bool)) rho O (@None (string bool))) (V O)) (@eval (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB (@update (option (string bool)) rho O (@None (string bool))) (V O)) *)
    intros H'. cbn. apply H, (IB_F H').
  - rewrite <- BPCP_BPCP'. intros H1 H2 % (BPCP_valid R (b:=full)).
(* Goal: False *)
    apply (valid_satis H2), H1.
Qed.



(** ** Corollaries *)

Lemma form_discrete {b : logic} :
  discrete (form b).
Proof.
(* Goal: discrete (form b) *)
  apply discrete_iff. constructor. apply eq_dec_form.
Qed.

Hint Resolve stack_enum form_discrete.

Definition UA :=
  ~ enumerable (compl BPCP).

Corollary valid_red :
  BPCP ⪯ @valid frag.
Proof.
(* Goal: @reduces (list (card bool)) (form frag) BPCP (@prv intu frag (@nil (form frag))) *)
  exists (fun R => F R). intros R. apply (BPCP_valid R).
Qed.

Corollary valid_undec :
  UA -> ~ decidable (@valid frag).
Proof.
(* Goal: @sat (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB full rho (@Impl full (@All full O (@Impl full (@Pr full (V O) (V O)) Fal)) Fal) *)
  intros H. now apply (not_decidable valid_red).
Qed.

Corollary valid_unenum :
  UA -> ~ enumerable (compl (@valid frag)).
Proof.
(* Goal: @sat (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB full rho (@Impl full (@All full O (@Impl full (@Pr full (V O) (V O)) Fal)) Fal) *)
  intros H. now apply (not_coenumerable valid_red).
Qed.

Corollary prv_red :
  BPCP ⪯ @prv intu frag nil.
Proof.
(* Goal: @reduces (list (card bool)) (form frag) BPCP (@prv intu frag (@nil (form frag))) *)
  exists (fun R => F R). intros R. apply (BPCP_prv R).
Qed.

Corollary prv_undec :
  UA -> ~ decidable (@prv intu frag nil).
Proof.
(* Goal: @sat (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB full rho (@Impl full (@All full O (@Impl full (@Pr full (V O) (V O)) Fal)) Fal) *)
  intros H. now apply (not_decidable prv_red).
Qed.

Corollary prv_unenum :
  UA -> ~ enumerable (compl (@prv intu frag nil)).
Proof.
(* Goal: @sat (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB full rho (@Impl full (@All full O (@Impl full (@Pr full (V O) (V O)) Fal)) Fal) *)
  intros H. apply (not_coenumerable prv_red); trivial.
Qed.

Corollary satis_red :
  compl BPCP ⪯ @satis full.
Proof.
(* Goal: forall x : list (card bool), iff (@compl (list (card bool)) BPCP x) (@satis full (@Impl full (@F full x) Fal)) *)
  exists (fun R => ¬ F R). intros R. apply (BPCP_satis R).
Qed.

Corollary satis_undec :
  UA -> ~ decidable (@satis full).
Proof.
(* Goal: forall _ : UA, not (@decidable (form full) (@satis full)) *)
  intros H1 H2 % (dec_red satis_red).
(* Goal: False *)
  now apply H1, dec_count_enum.
Qed.

Corollary satis_enum :
  UA -> ~ enumerable (@satis full).
Proof.
(* Goal: forall _ : UA, not (@enumerable (form full) (@satis full)) *)
  intros H1 H2 % (enumerable_red satis_red); auto.
Qed.


  





(** ** Non-Standard Model *)

Module NonStan. Section Nonstan.

  Variable R : BSRS.

  Instance IB : interp (option (string bool)) (fun _ => Some nil) :=
    {|
      i_f b x := match x with Some u => Some (b :: u) | None => None end ;
      i_e := Some nil;
      i_P x y := match x, y with Some u, Some v => derivable R u v | _, _ => True end ;
      i_Q := False
    |}.

  Lemma IB_eval_Some rho t u v :
    eval rho t = Some v -> eval rho (prep u t) = Some (u ++ v).
  Proof.
(* Goal: @sat (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB full rho (@Impl full (@All full O (@Impl full (@Pr full (V O) (V O)) Fal)) Fal) *)
    intros H. induction u; cbn; trivial.
(* Goal: @eq (option (string bool)) match @eval (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB rho (@fold_right term bool t_f t u) with | Some u => @Some (list bool) (@cons bool a u) | None => @None (list bool) end (@None (string bool)) *)
    unfold prep in IHu. now rewrite IHu.
  Qed.

  Lemma IB_eval_None rho t u :
    eval rho t = None -> eval rho (prep u t) = None.
  Proof.
(* Goal: @sat (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB full rho (@Impl full (@All full O (@Impl full (@Pr full (V O) (V O)) Fal)) Fal) *)
    intros H. induction u; cbn; trivial.
(* Goal: @eq (option (string bool)) match @eval (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB rho (@fold_right term bool t_f t u) with | Some u => @Some (list bool) (@cons bool a u) | None => @None (list bool) end (@None (string bool)) *)
    unfold prep in IHu. now rewrite IHu.
  Qed.

  Lemma IB_enc rho u :
    eval rho (enc u) = Some u.
  Proof.
(* Goal: @eq (string bool) (@eval (string bool) (fun _ : nat => @nil bool) IB rho (enc s)) s *)
    unfold enc. rewrite <- (app_nil_r u) at 2.
    now apply IB_eval_Some.
  Qed.

  Lemma IB_deriv rho u v :
    rho ⊨ (Pr (enc u) (enc v)) <-> derivable R u v.
  Proof.
(* Goal: iff (@derivable bool R u v) (@derivable bool R u v) *)
    cbn. rewrite !IB_enc. reflexivity.
  Qed.

  Lemma IB_deriv' rho t1 t2 u v :
    eval rho t1 = Some u -> eval rho t2 = Some v ->
    rho ⊨ (Pr t1 t2) <-> derivable R u v.
  Proof.
(* Goal: iff (@derivable bool R u v) (@derivable bool R u v) *)
    intros H1 H2. cbn. rewrite H1, H2. reflexivity.
  Qed.

  Lemma IB_F1 rho :
    rho ⊫ F1 R.
  Proof.
(* Goal: forall (psi : form b) (_ : @In (form b) psi F1), @sat (string bool) (fun _ : nat => @nil bool) IB b rho psi *)
    unfold F1. 
(* Goal: forall (psi : form b) (_ : @In (form b) psi (@map (prod (string bool) (string bool)) (form b) (fun '(pair x y) => @Pr b (enc x) (enc y)) R)), @sat (string bool) (fun _ : nat => @nil bool) IB b rho psi *)
    intros ? ([x y] & <- & ?) % in_map_iff.
(* Goal: @i_P (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB (@eval (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB (@update (option (string bool)) rho O (@None (string bool))) (V O)) (@eval (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB (@update (option (string bool)) rho O (@None (string bool))) (V O)) *)
    cbn. rewrite !IB_enc. now constructor.
  Qed.

  Lemma IB_F2 rho :
    rho ⊫ F2 R.
  Proof.
(* Goal: forall (psi : form b) (_ : @In (form b) psi F2), @sat (string bool) (fun _ : nat => @nil bool) IB b rho psi *)
    unfold F2. intros ? ([x y] & <- & ?) % in_map_iff [u|] [v|] ?; cbn in *.
    - erewrite !IB_eval_Some; cbn; auto. now constructor 2.
    - erewrite IB_eval_Some, IB_eval_None; cbn; auto.
    - erewrite IB_eval_None; cbn; auto.
    - erewrite !IB_eval_None; cbn; auto.
  Qed.

  Lemma IB_F rho :
    rho ⊨ F R.
  Proof.
(* Goal: forall _ : @derivable bool R u v, @sat domain eta I b rho (@impl b F1 (@impl b F2 (@Pr b (enc u) (enc v)))) *)
    unfold F. rewrite !impl_sat. intros _ _ H.
(* Goal: @i_P (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB (@eval (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB (@update (option (string bool)) rho O (@None (string bool))) (V O)) (@eval (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB (@update (option (string bool)) rho O (@None (string bool))) (V O)) *)
    apply (H None). cbn. auto.
  Qed.

  Lemma IB_nonstandard rho :
    rho ⊨ ¬ ∀ 0; ¬ Pr 0 0.
  Proof.
(* Goal: @i_P (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB (@eval (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB (@update (option (string bool)) rho O (@None (string bool))) (V O)) (@eval (option (string bool)) (fun _ : nat => @Some (list bool) (@nil bool)) IB (@update (option (string bool)) rho O (@None (string bool))) (V O)) *)
    intros H. apply (H None). cbn. auto.
  Qed.

End Nonstan. End NonStan.
