Require Import FOL.Proofmode.StringToIdent.
From Equations Require Import Equations.
Require Import Equations.Type.DepElim.
From Undecidability.Shared Require Import Dec ListAutomation.
From FOL Require Import FullSyntax.
From FOL.Proofmode Require Import Theories.

Require Import List Lia String.
Import ListNotations.
Import ListAutomationNotations ListAutomationFacts ListAutomationHints ListAutomationInstances.

Open Scope string_scope.

Definition pm {p cf cp ff} C phi := @prv p cf cp ff C phi.
Arguments pm {_} {_} {_} {_} _ _.

Definition tpm {p cf cp ff} C phi := @tprv p cf cp ff C phi.
Arguments tpm {_} {_} {_} {_} _ _.

Section PM.

Context {Σ_funcs : funcs_signature}.
Context {Σ_preds : preds_signature}.
Context {ff : falsity_flag}.

Definition cnil := @nil form.
Definition ccons (s : string) phi C := @cons form phi C.
Definition cblackbox (A : list form) := A.

Definition tnil : theory := fun _ => False.
Definition tcons (s : string) phi (T : theory) : theory := extend T phi.
Definition tblackbox (T : theory) := T.

End PM.

Ltac custom_fold := idtac.

 Ltac custom_unfold := idtac.

Ltac custom_simpl := idtac.


Class DeductionRules `{funcs_signature, preds_signature, falsity_flag} (context : Type) (ent : context -> form -> Type) (cons : form -> context -> context) (map : (form -> form) -> context -> context) (In : form -> context -> Prop) :=
{
  II A phi psi : ent (cons phi A) psi -> ent A (phi → psi) ;
  IE A phi psi : ent A (phi → psi) -> ent A phi -> ent A psi ;
  AllI A phi : ent (map (subst_form ↑) A) phi -> ent A (∀ phi) ;
  AllE A t phi : ent A (∀ phi) -> ent A (phi[t..]) ;
  ExI A t phi : ent A (phi[t..]) -> ent A (∃ phi) ;
  ExE A phi psi : ent A (∃ phi) -> ent (cons phi (map (subst_form ↑) A)) (psi[↑]) -> ent A psi ;
  Ctx A phi : In phi A -> ent A phi ;
  CI A phi psi : ent A phi -> ent A psi -> ent A (phi ∧ psi) ;
  CE1 A phi psi : ent A (phi ∧ psi) -> ent A phi ;
  CE2 A phi psi : ent A (phi ∧ psi) -> ent A psi ;
  DI1 A phi psi : ent A phi -> ent A (phi ∨ psi) ;
  DI2 A phi psi : ent A psi -> ent A (phi ∨ psi) ;
  DE A phi psi theta : ent A (phi ∨ psi) -> ent (cons phi A) theta -> ent (cons psi A) theta -> ent A theta ;
}.
Arguments DeductionRules {_} {_} {_} _ _ _ _ _.

Class ClassicalDeductionRules `{funcs_signature, preds_signature, falsity_flag} (context : Type) (ent : context -> form -> Type) :=
{
  Pc A phi psi : ent A (((phi → psi) → phi) → phi)
}.
Arguments ClassicalDeductionRules {_} {_} {_} _ _.

Class FalsityDeductionRules `{funcs_signature, preds_signature} (context : Type) (ent : context -> form -> Type) :=
{
  Exp A phi : ent A ⊥ -> ent A phi ;
}.
Arguments FalsityDeductionRules {_} {_} _ _.

Class WeakClass `{funcs_signature, preds_signature, falsity_flag} (context : Type) (ent : context -> form -> Type) (incl : context -> context -> Prop) :=
{
  Weak A B phi : ent A phi -> incl A B -> ent B phi
}.
Arguments WeakClass {_} {_} {_} _ _.

#[global]
Instance prv_DeductionRules `{funcs_signature, preds_signature, falsity_flag, peirce} : DeductionRules (list form) prv cons (@List.map form form) (@In form) :=
{|
  II := FullND.II ;
  IE := FullND.IE ;
  AllI := FullND.AllI ;
  AllE := FullND.AllE ;
  ExI := @FullND.ExI _ _ _ _;
  ExE := FullND.ExE ;
  Ctx := FullND.Ctx ;
  CI := FullND.CI ;
  CE1 := FullND.CE1 ;
  CE2 := FullND.CE2 ;
  DI1 := FullND.DI1 ;
  DI2 := FullND.DI2 ;
  DE := FullND.DE ;
|}.

#[global]
Instance prv_ClassicalDeductionRules `{funcs_signature, preds_signature, falsity_flag} : ClassicalDeductionRules (list form) (@prv _ _ _ class) :=
{|
  Pc := FullND.Pc
|}.

#[global]
Instance prv_FalsityDeductionRules `{funcs_signature, preds_signature, peirce} : FalsityDeductionRules (list form) (@prv _ _ falsity_on _) :=
{|
  Exp := FullND.Exp
|}.

#[global]
Instance prv_WeakClass `{funcs_signature, preds_signature, falsity_flag, peirce} : WeakClass (list form) prv (@List.incl form) :=
{|
  Weak := FullNDFacts.Weak
|}.


#[global]
Instance eq_dec_full_operators : eq_dec binop. unfold dec; decide equality. Qed.
#[global]
Instance eq_dec_full_logic_quant : eq_dec quantop. unfold dec; decide equality. Qed.

#[global]
Instance tprv_DeductionRules `{funcs_signature, preds_signature, falsity_flag, peirce, eq_dec syms, eq_dec preds} : DeductionRules theory tprv (fun a b => extend b a) mapT (fun a b => in_theory b a) :=
{|
  II := Theories.T_II ;
  IE := Theories.T_IE ;
  AllI := Theories.T_AllI ;
  AllE := Theories.T_AllE ;
  ExI := Theories.T_ExI ;
  ExE := Theories.T_ExE ;
  Ctx := Theories.T_Ctx ;
  CI := Theories.T_CI ;
  CE1 := Theories.T_CE1 ;
  CE2 := Theories.T_CE2 ;
  DI1 := Theories.T_DI1 ;
  DI2 := Theories.T_DI2 ;
  DE := Theories.T_DE ;
|}.

#[global]
Instance tprv_ClassicalDeductionRules `{funcs_signature, preds_signature, falsity_flag} : ClassicalDeductionRules theory (@tprv _ _ _ class) :=
{|
  Pc := Theories.T_Pc
|}.

#[global]
Instance tprv_FalsityDeductionRules `{funcs_signature, preds_signature, peirce} : FalsityDeductionRules theory (@tprv _ _ falsity_on _) :=
{|
  Exp := Theories.T_Exp
|}.

#[global]
Instance tprv_WeakClass `{funcs_signature, preds_signature, falsity_flag, peirce} : WeakClass theory tprv subset_T :=
{|
  Weak := Theories.WeakT
|}.


Definition digit_to_string n := match n with
  | 0 => "0" | 1 => "1" | 2 => "2" | 3 => "3" | 4 => "4" | 5 => "5"
  | 6 => "6" | 7 => "7" | 8 => "8" | 9 => "9" | _ => "_"
end.
Fixpoint nat_to_string' fuel n := match fuel with
  | 0 => "OUT OF FUEL"
  | S fuel' => match n with
    | 0 => ""
    | _ => nat_to_string' fuel' (Nat.div n 10) ++ digit_to_string (Nat.modulo n 10)
    end
end.
Definition nat_to_string n := match n with 0 => "0" | _ => nat_to_string' 100 n end.

Ltac lookup' n C name :=
  match C with
  | ccons name _ _ => constr:(Some n)
  | ccons _ _ ?C' => lookup' (S n) C' name
  | tcons name _ _ => constr:(Some n)
  | tcons _ _ ?T' => lookup' (S n) T' name
  | _ => None
  end.
Ltac lookup := lookup' 0.

Ltac nth A n :=
  match n with
  | 0 => match A with ?t :: _ => t | extend _ ?t => t | ccons _ ?t _ => t | tcons _ ?t _ => t end
  | S ?n' => match A with _ :: ?A' => nth A' n' | extend ?A' _ => nth A' n' | ccons _ _ ?A' => nth A' n' | tcons _ _ ?T' => nth T' n' end
  end.

Ltac remove A n :=
  match n with
  | 0 => match A with _ :: ?A' => A' | extend ?A' _ => A' | ccons _ _ ?A' => A' | tcons _ _ ?A' => A' end
  | S ?n' => match A with
    | ?t :: ?A' => let A'' := remove A' n' in constr:(t::A'')
    | extend ?A' ?t => let A'' := remove A' n' in constr:(extend t A'')
    | ccons ?s ?t ?A' => let A'' := remove A' n' in constr:(ccons s t A'')
    | tcons ?s ?t ?A' => let A'' := remove A' n' in constr:(tcons s t A'')
    end
  end.

Ltac replace_ltac A n phi :=
  match n with
  | 0 => match A with _ :: ?A' => constr:(phi::A') | extend ?A' _ => constr:(extend A' phi) | ccons ?s _ ?A' => constr:(ccons s phi A') | tcons ?s _ ?A' => constr:(tcons s phi A') end
  | S ?n' => match A with
    | ?t :: ?A' => let A'' := replace_ltac A' n' phi in constr:(t::A'')
    | extend ?A' ?t => let A'' := replace_ltac A' n' phi in constr:(extend t A'')
    | ccons ?s ?t ?A' => let A'' := replace_ltac A' n' phi in constr:(ccons s t A'')
    | tcons ?s ?t ?A' => let A'' := replace_ltac A' n' phi in constr:(tcons s t A'')
    end
  end.

Ltac map_ltac A f :=
  match A with
  | nil => constr:(nil)
  | cnil => constr:(cnil)
  | tnil => constr:(tnil)
  | @Vector.nil ?a => constr:(@Vector.nil a)
  | cblackbox ?A' => A
  | tblackbox ?A' => A
  | cons ?x ?A' => let x' := f x in let A'' := map_ltac A' f in constr:(cons x' A'')
  | ccons ?s ?x ?A' => let x' := f x in let A'' := map_ltac A' f in constr:(ccons s x' A'')
  | tcons ?s ?x ?A' => let x' := f x in let A'' := map_ltac A' f in constr:(tcons s x' A'')
  | @Vector.cons _ ?x _ ?A' => let x' := f x in let A'' := map_ltac A' f in constr:(@Vector.cons _ x' _ A'')
  end.

Ltac new_name' n base C :=
  let name := match n with
    | 0 => base
    | S ?n' => let s := eval cbn in (nat_to_string n') in eval cbn in (base ++ s)
  end in
  match lookup C name with
  | @None => name
  | @Some _ _ => new_name' (S n) base C
  end.
Ltac new_name base C := new_name' 0 base C.

Ltac create_context' A :=
  match A with
  | ?phi::?A' =>
    let x := create_context' A' in match x with (?c, ?n) =>
      match n with
        | 0 => constr:((ccons "H" phi c, S n))
        | S ?n' => let s' := eval cbn in ("H" ++ nat_to_string n') in constr:((ccons s' phi c, S n))
      end
    end
  | extend ?T' ?phi =>
    let x := create_context' T' in match x with (?c, ?n) =>
      match n with
        | 0 => constr:((tcons "H" phi c, S n))
        | S ?n' => let s' := eval cbn in ("H" ++ nat_to_string n') in constr:((tcons s' phi c, S n))
      end
    end
  | nil => constr:((cnil, 0))
  | _ =>
    
    match type of A with
    | list form => constr:((cblackbox A, 0))
    | theory => constr:((tblackbox A, 0))
    | form -> Prop => constr:((tblackbox A, 0))
    end
  end.
Ltac create_context A := let x := create_context' A in match x with (?c, _) => c end.


Ltac solve_list_incl :=
  try (repeat (try apply incl_refl; apply incl_tl)); firstorder.


Inductive ident_name := Ident : (unit -> unit) -> ident_name.

Ltac to_ident_name id :=
  eval cbv in (ltac:(clear; apply Ident; intros id; assumption) : ident_name).

Notation "x" := (Ident (fun x => x)) (at level 1, only printing).

Definition named_quant {fsig psig ops ff} op (x : ident_name) phi := @quant fsig psig ops ff op phi.
Definition named_var {fsig} n (x : ident_name) := @var fsig n.
Arguments named_var {_ _} _.

Ltac assert_is_constant_nat n :=
  match n with
    | 0 => 0
    | S ?n => assert_is_constant_nat n
  end.

Ltac annotate_term f t :=
  match t with
    | context C[ var ?n ] =>
        let _ := assert_is_constant_nat n in
        let ident_name := eval cbn in (f n) in
        let t' := context C[ @named_var _ n ident_name ] in
        annotate_term f t'
    | _ => t
  end.

Ltac annotate_form' f idx phi :=
  match phi with
  | falsity => constr:(falsity)
  | atom ?P ?v =>
      let map_fun := annotate_term f in
      let v' := map_ltac v map_fun in
      constr:(atom P v')
  | bin ?op ?psi1 ?psi2 =>
      let psi1' := annotate_form' f idx psi1 in
      let psi2' := annotate_form' f idx psi2 in
      constr:(bin op psi1' psi2')
  | quant ?op ?psi =>
      let name := eval cbn in ("x" ++ nat_to_string idx) in
      let id := string_to_ident name in
      
      match phi with
      | _ =>
          let _ := eval cbv in ltac:(assert (id := 0); clear id; exact 0) in
          let ident_name := to_ident_name id in
          let f' := constr:(fun n => match n with 0 => ident_name | S n' => f n' end) in
          let psi' := annotate_form' f' (S idx) psi in
          constr:(named_quant op ident_name psi')
      | _ => annotate_form' f (S idx) phi
      end
  
  | _ =>
      match phi with
      | context C[ var ?n ] =>
          let _ := assert_is_constant_nat n in
          let ident_name := eval cbn in (f n) in
          let phi' := context C[ @named_var _ n ident_name ] in
          annotate_form' f idx phi'
      | _ => phi
      end
  end.

Ltac add_binder_names :=
  match goal with
  | [ |- @pm _ _ _ ?p ?C ?phi ] =>
    let f := constr:(fun (n : nat) => Ident (fun _unknown => _unknown)) in
    let annotate_form := annotate_form' f 0 in
    let phi' := annotate_form phi in
    let C' := map_ltac C annotate_form in
    change (@pm _ _ _ p C' phi')
  | [ |- @tpm _ _ _ ?p ?C ?phi ] =>
    let f := constr:(fun (n : nat) => Ident (fun _unknown => _unknown)) in
    let annotate_form := annotate_form' f 0 in
    let phi' := annotate_form phi in
    let C' := map_ltac C annotate_form in
    change (@tpm _ _ _ p C' phi')
  end.
Ltac update_binder_names := unfold named_quant; unfold named_var; add_binder_names.


Notation "" := cnil (only printing).
Notation "A" := (cblackbox A) (at level 1, only printing, format " A").
Notation "C name : phi" := (ccons name phi C)
  (at level 1, C at level 200, phi at level 200,
  left associativity, format "C '//' name : '[' phi ']'", only printing).

Notation "" := tnil (only printing).
Notation "A" := (tblackbox A) (at level 1, only printing, format " A").
Notation "C name : phi" := (tcons name phi C)
  (at level 1, C at level 200, phi at level 200,
  left associativity, format "C '//' name : '[' phi ']'", only printing).

Notation "∀ x .. y , phi" := (named_quant All x ( .. (named_quant All y phi) .. )) (at level 50, only printing,
  format "'[' '∀' '/ ' x .. y , '/ ' phi ']'").
Notation "∃ x .. y , phi" := (named_quant Ex x ( .. (named_quant Ex y phi) .. )) (at level 50, only printing,
  format "'[' '∃' '/ ' x .. y , '/ ' phi ']'").

Notation "x" := (named_var (Ident (fun x => x))) (at level 1, only printing).

Notation "C '━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━' phi" :=
  (pm C phi)
  (at level 1, left associativity,
  format " C '//' '━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━' '//' phi", only printing).

Notation "T '━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━' phi" :=
  (tpm T phi)
  (at level 1, left associativity,
  format " T '//' '━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━' '//' phi", only printing).

Ltac fstart :=
  match goal with
  | [ |- @prv _ _ _ ?p ?A ?phi ] => let C := create_context A in change (@pm _ _ _ p C phi)
  | [ |- @tprv _ _ _ ?p ?T ?phi ] => let C := create_context T in change (@tpm _ _ _ p C phi)
  end;
  add_binder_names.
Ltac fstop :=
  match goal with
  | [ |- @pm _ _ _ ?p ?C ?phi ] => change (@prv _ _ _ p C phi)
  | [ |- @tpm _ _ _ ?p ?C ?phi ] => change (@tprv _ _ _ p C phi)
  end;
  unfold pm in *; unfold cnil; unfold ccons;unfold cblackbox;
  unfold tpm in *; unfold tnil; unfold tcons;unfold tblackbox;
  unfold named_quant; unfold named_var.


Ltac make_compatible tac :=
  match goal with
  | [ |- prv ?A _ ] => tac A
  | [ |- tprv ?T _ ] => tac T
  | [ |- @pm _ _ _ ?p ?C _ ] =>
      fstop;
      tac C;
      match goal with
      | [ |- pm _ _ ?G ] => change (@pm _ _ _ p C G)
      | [ |- prv _ ?G ] => change (@pm _ _ _ p C G)
      | _ => idtac
      end;
      try update_binder_names
  | [ |- @tpm _ _ ?p ?C _ ] =>
      fstop;
      tac C;
      match goal with
      | [ |- tprv _ ?G ] => change (@tpm _ _ p C G)
      | _ => idtac
      end;
      try update_binder_names
  end.

Ltac make_compatible_light tac :=
  match goal with
  | [ |- prv ?A _ ] => tac A
  | [ |- tprv ?T _ ] => tac T
  | [ |- @pm _ _ _ ?p ?C _ ] =>
      fstop;
      tac C;
      match goal with
      | [ |- pm _ _ ?G ] => change (@pm _ _ _ p C G)
      | [ |- prv _ ?G ] => change (@pm _ _ _ p C G)
      | _ => idtac
      end
  | [ |- @tpm _ _ ?p ?C _ ] =>
      fstop;
      tac C;
      match goal with
      | [ |- tprv _ ?G ] => change (@tpm _ _ p C G)
      | _ => idtac
      end
  end.

Ltac assert_compat' phi H :=
  match goal with
  | [ |- ?C ⊢ _ ] => assert (@prv _ _ _ C phi) as H
  | [ |- ?C ⊩ _ ] => assert (@tprv _ _ _ C phi) as H
  | [ |- @pm _ _ _ _ ?C _ ] => assert (@pm _ _ _ _ C phi) as H
  | [ |- @tpm _ _ _ _ ?C _ ] => assert (@tpm _ _ _ _ C phi) as H
  end.
Tactic Notation "assert_compat" constr(phi) := let H := fresh in assert_compat' phi H.
Tactic Notation "assert_compat" constr(phi) "as" ident(H) := assert_compat' phi H.
Tactic Notation "assert_compat" constr(phi) "by" tactic(tac) := let H := fresh in assert_compat' phi H; [tac|].
Tactic Notation "assert_compat" constr(phi) "as" ident(H) "by" tactic(tac) := assert_compat' phi H; [tac|].

Ltac enough_compat' phi H :=
  match goal with
  | [ |- ?C ⊢ _ ] => enough (@prv _ _ _ C phi) as H
  | [ |- ?C ⊩ _ ] => enough (@tprv _ _ _ C phi) as H
  | [ |- @pm _ _ _ _ ?C _ ] => enough (@pm _ _ _ _ C phi) as H
  | [ |- @tpm _ _ _ _ ?C _ ] => enough (@tpm _ _ _ _ C phi) as H
  end.
Tactic Notation "enough_compat" constr(phi) := let H := fresh in enough_compat' phi H.
Tactic Notation "enough_compat" constr(phi) "as" ident(H) := enough_compat' phi H.
Tactic Notation "enough_compat" constr(phi) "by" tactic(tac) := let H := fresh in enough_compat' phi H; [tac|].
Tactic Notation "enough_compat" constr(phi) "as" ident(H) "by" tactic(tac) := enough_compat' phi H; [tac|].

Ltac apply_compat' H1 H2 :=
  match goal with
  | [ |- _ ⊢ _ ] => apply H1
  | [ |- _ ⊩ _ ] => apply H2
  end.
Ltac apply_compat_in H1 H2 H :=
  match goal with
  | [ |- _ ⊢ _ ] => apply H1 in H
  | [ |- _ ⊩ _ ] => apply H2 in H
  end.
Tactic Notation "apply_compat" constr(H1) constr(H2) := apply_compat' H1 H2.
Tactic Notation "apply_compat" constr(H1) constr(H2) "in" hyp(H) := apply_compat_in H1 H2 H.

Ltac get_context_goal :=
  match goal with
  | [ |- ?C ⊢ _ ] => C
  | [ |- ?C ⊩ _ ] => C
  | [ |- pm ?C _ ] => C
  | [ |- tpm ?C _ ] => C
  end.
Ltac get_context_hyp H :=
  match type of H with
  | ?C ⊢ _ => C
  | ?C ⊩ _ => C
  | pm ?C _ => C
  | tpm ?C _ => C
  end.
Tactic Notation "get_context" := get_context_goal.
Tactic Notation "get_context" hyp(H) := get_context_hyp H.

Ltac get_form_goal :=
  match goal with
  | [ |- _ ⊢ ?phi ] => phi
  | [ |- _ ⊩ ?phi ] => phi
  | [ |- pm _ ?phi ] => phi
  | [ |- tpm _ ?phi ] => phi
  end.
Ltac get_form_hyp H :=
  match type of H with
  | _ ⊢ ?phi => phi
  | _ ⊩ ?phi => phi
  | pm _ ?phi => phi
  | tpm _ ?phi => phi
  end.
Tactic Notation "get_form" := get_form_goal.
Tactic Notation "get_form" hyp(H) := get_form_hyp H.


#[global]
Hint Rewrite -> @up_term : subst.
#[global]
Hint Rewrite -> @subst_term_shift : subst.
#[global]
Hint Rewrite -> @up_form : subst.
#[global]
Hint Rewrite -> @subst_shift : subst.

Ltac simpl_subst_hyp H :=
  cbn in H;
  repeat match type of H with
  | context C[fun x => $(S x)] => let H' := context C[↑] in change H' in H
  | context C[S >> var] => let H' := context C[↑] in change H' in H
  end;
  try rewrite !up_term in H;
  try rewrite !subst_term_shift in H;
  try rewrite !up_form in H;
  try rewrite !subst_shift in H;
  
  unfold ">>";
  
  repeat match goal with
  | [ |- context C[fun x => $(S x)] ] => let H' := context C[↑] in change H' in H
  end;
  
  custom_fold;
  custom_simpl.

Ltac simpl_subst_goal :=
  cbn;
  repeat match goal with
  | [ |- context C[fun x => $(S x)] ] => let G := context C[↑] in change G
  | [ |- context C[S >> var] ] => let G := context C[↑] in change G
  end;
  try rewrite !up_term;
  try rewrite !subst_term_shift;
  try rewrite !up_form;
  try rewrite !subst_shift;
  
  unfold ">>";
  
  repeat match goal with
  | [ |- context C[fun x => $(S x)] ] => let G := context C[↑] in change G
  end;
  
  custom_fold;
  custom_simpl.

Tactic Notation "simpl_subst" hyp(H) := (simpl_subst_hyp H).
Tactic Notation "simpl_subst" := (simpl_subst_goal).

Ltac eval_mapT M :=
  match M with
  | mapT ?f (extend ?T ?a) => let T' := eval_mapT (mapT f T) in constr:(extend T' (f a))
  | mapT ?f (tcons ?s ?a ?T) => let T' := eval_mapT (mapT f T) in constr:(tcons s (f a) T')
  | mapT ?f (tblackbox ?T) => constr:(tblackbox (mapT f T))
  | _ => M
  end.

Lemma mapT_step `{s1 : funcs_signature, s2 : preds_signature, ff : falsity_flag, p : peirce} f a T1 T2 :
  subset_T T1 (mapT f T2) -> subset_T (extend T1 (f a)) (mapT f (extend T2 a)).
Proof.
  intros H psi H1. destruct H1 as [H1|H1].
  - destruct (H psi H1) as [rho [H2 H3]]. exists rho. split. now left. assumption.
  - exists a. split. now right. auto.
Qed.

Ltac simpl_context_mapT :=
  match goal with
  | [ |- tprv ?T ?phi ] =>
      let T' := eval_mapT T in
      let X := fresh in
      enough (tprv T' phi) as X; [
        eapply Weak; [now apply X | repeat apply mapT_step; apply subset_refl ]
      |]
  | [ |- tpm ?T ?phi ] =>
      let T' := eval_mapT T in
      let X := fresh in
      enough (tpm T' phi) as X; [
        eapply Weak; [now apply X | repeat apply mapT_step; apply subset_refl ]
      |]
  end.


Ltac ctx := make_compatible ltac:(fun _ => apply Ctx; firstorder).

Ltac fexfalso := make_compatible ltac:(fun _ => apply Exp).
Ltac fsplit := make_compatible ltac:(fun _ => apply CI).
Ltac fleft := make_compatible ltac:(fun _ => apply DI1).
Ltac fright := make_compatible ltac:(fun _ => apply DI2).


Section IntroPattern.
  Import Ascii.

  Inductive intro_pattern :=
    | patId : string -> intro_pattern
    | patAnd : intro_pattern -> intro_pattern -> intro_pattern
    | patOr : intro_pattern -> intro_pattern -> intro_pattern
    | patRewrite : intro_pattern
    | patRewriteBack : intro_pattern.

  Fixpoint read_name s := match s with
  | String "]" s' => ("", String "]" s')
  | String " " s' => ("", String " " s')
  | String "|" s' => ("", String "|" s')
  | String c s' => let (a, s'') := read_name s' in (String c a, s'')
  | EmptyString => ("", EmptyString)
  end.

  Fixpoint parse_intro_pattern' s fuel := match fuel with
  | 0 => (None, s)
  | S fuel' =>
    match s with
    | String ("[") s' =>
        match parse_intro_pattern' s' fuel' with
        | (Some p1, String "|" s'') => match parse_intro_pattern' s'' fuel' with
                                      | (Some p2, String "]" s''') => (Some (patOr p1 p2), s''')
                                      | _ => (None, "")
                                      end
        | (Some p1, String " " s'') => match parse_intro_pattern' s'' fuel' with
                                      | (Some p2, String "]" s''') => (Some (patAnd p1 p2), s''')
                                      | _ => (None, "")
                                      end
        | _ => (None, "")
        end
    | String ("]") s' => (Some (patId "?"), String "]" s')
    | String " " s' => (Some (patId "?"), String " " s')
    | String "|" s' => (Some (patId "?"), String "|" s')
    | String "-" (String ">" s') => (Some patRewrite, s')
    | String "<" (String "-" s') => (Some patRewriteBack, s')
    | EmptyString => (None, EmptyString)
    | s => let (a, s') := read_name s in (Some (patId a), s')
    end
  end.
  Definition parse_intro_pattern s := fst (parse_intro_pattern' s 100).

End IntroPattern.

Ltac create_pattern T :=
  match T with
  | ?t ∧ ?s => constr:(patAnd (patId "?") (patId "?"))
  | ?t ∨ ?s => constr:(patOr (patId "?") (patId "?"))
  | ∃ ?t => constr:(patAnd (patId "?") (patId "?"))
  | named_quant Ex _ ?t => constr:(patAnd (patId "?") (patId "?"))
  | _ => constr:(patId "?")
  end.

Ltac create_deep_pattern T :=
  match T with
  | ?t ∧ ?s =>
    let p1 := create_deep_pattern t in
    let p2 := create_deep_pattern s in
    constr:(patAnd p1 p2)
  | ?t ∨ ?s =>
    let p1 := create_deep_pattern t in
    let p2 := create_deep_pattern s in
    constr:(patOr p1 p2)
  | ∃ ?t =>
    let p1 := constr:(patId "?") in
    let p2 := create_deep_pattern t in
    constr:(patAnd p1 p2)
  | named_quant Ex _ ?t =>
    let p1 := constr:(patId "?") in
    let p2 := create_deep_pattern t in
    constr:(patAnd p1 p2)
  | _ => constr:(patId "?")
  end.

Section Fintro.
  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.
  Context {ff : falsity_flag}.
  Variable p : peirce.

  Lemma intro_and_destruct A s t G :
    A ⊢ (s → t → G) -> A ⊢ (s ∧ t → G).
  Proof.
    intros. now apply switch_conj_imp.
  Qed.

  Lemma intro_or_destruct A s t G :
    A ⊢ (s → G) -> A ⊢ (t → G) -> A ⊢ (s ∨ t → G).
  Proof.
    intros Hs Ht. apply II. eapply DE. ctx.
    eapply Weak in Hs. eapply IE. apply Hs. ctx. firstorder.
    eapply Weak in Ht. eapply IE. apply Ht. ctx. firstorder.
  Qed.

  Context {eq_dec_Funcs : eq_dec syms}.
  Context {eq_dec_Preds : eq_dec preds}.

  Lemma intro_and_destruct_T T s t G :
    T ⊩ (s → t → G) -> T ⊩ (s ∧ t → G).
  Proof.
    intros. apply II. apply (IE (phi := t)). apply (IE (phi := s)).
    eapply Weak. apply H. firstorder.
    eapply CE1, Ctx; firstorder.
    eapply CE2, Ctx; firstorder.
  Qed.

  Lemma intro_or_destruct_T T s t G :
    T ⊩ (s → G) -> T ⊩ (t → G) -> T ⊩ (s ∨ t → G).
  Proof.
    intros Hs Ht. apply II. eapply DE. ctx.
    eapply Weak in Hs. eapply IE. apply Hs. ctx. firstorder.
    eapply Weak in Ht. eapply IE. apply Ht. ctx. firstorder.
  Qed.

  Lemma subst_zero phi x :
    $0 = x -> phi = phi[fun n => match n with 0 => x | S n => $(S n) end].
  Proof.
    intros. symmetry. apply subst_id. intros [|]; cbn. now rewrite H. reflexivity.
  Qed.

  Lemma subst_zero_term t x :
    $0 = x -> t`[fun n => match n with 0 => x | S n => $(S n) end] = t.
  Proof.
    intros. apply subst_term_id. intros [|]; cbn. now rewrite H. reflexivity.
  Qed.

End Fintro.

Ltac hypname_from_pattern C id :=
  match id with
  | "?" => new_name "H" C
  | _ => match lookup C id with
    | @None => id
    | @Some _ _ => let msg := eval cbn in ("Identifier already used: " ++ id) in fail 7 msg
    end
  end.

Ltac varname_from_pat pat :=
  match pat with
  | patId "?" => fresh "x"
  | patId ?id => string_to_ident id
  end.

Ltac fintro_ident x :=
  let H := fresh "H" in
  match goal with
  | [ |- _ ⊢ ∀ ?t ] =>
    apply AllI;
    edestruct nameless_equiv_all as [x H];
    apply H; clear H;
    simpl_subst
  | [ |- @pm _ _ _ ?p ?C (named_quant All _ ?t) ] =>
    apply AllI;
    edestruct nameless_equiv_all as [x H];
    apply H; clear H;
    simpl_subst;
    match goal with [ |- prv _ ?t'] => change (@pm _ _ _ p C t') end;
    update_binder_names
  | [ |- @pm _ _ _ ?p ?C (quant All ?t) ] =>
    apply AllI;
    edestruct nameless_equiv_all as [x H];
    apply H; clear H;
    simpl_subst;
    match goal with [ |- prv _ ?t'] => change (@pm _ _ _ p C t') end;
    update_binder_names
  | [ |- _ ⊩ ∀ ?t ] =>
    let E := fresh "E" in
    apply AllI;
    assert (exists x, $0 = x) as [x E] by (now exists ($0));
    rewrite (subst_zero t x E);
    simpl_context_mapT;
    simpl_subst;
    repeat (try rewrite subst_zero_term; [| apply E]);
    clear E
  | [ |- @tpm _ _ _ ?p ?C (named_quant All _ ?t) ] =>
    let E := fresh "E" in
    apply AllI;
    assert (exists x, $0 = x) as [x E] by (now exists ($0));
    rewrite (subst_zero t x E);
    simpl_context_mapT;
    simpl_subst;
    repeat (try rewrite subst_zero_term; [| apply E]);
    clear E;
    update_binder_names
  | [ |- @tpm _ _ _ ?p ?C (quant All ?t) ] =>
    let E := fresh "E" in
    apply AllI;
    assert (exists x, $0 = x) as [x E] by (now exists ($0));
    rewrite (subst_zero t x E);
    simpl_context_mapT;
    simpl_subst;
    repeat (try rewrite subst_zero_term; [| apply E]);
    clear E;
    update_binder_names
  | _ =>
    
    progress custom_unfold; simpl_subst; try update_binder_names;
    custom_unfold;
    fintro_ident x;
    custom_fold
  end.

Ltac frewrite' T A back := fun contxt => idtac.

Ltac fintro_pat' pat :=
  match pat with
  | patAnd ?p1 ?p2 =>
      make_compatible_light ltac:(fun C =>
        apply II; eapply ExE; [ apply Ctx; now left |
          let x := varname_from_pat p1 in
          let H := fresh "H" in
          edestruct nameless_equiv_ex as [x H];
          apply <- H; clear H; cbn; simpl_subst; apply -> imps;
          eapply (@Weak _ _ _ _ _ _ _ C); [| now apply incl_tl] ]
      );
      fintro_pat' p2
  | patAnd ?p1 ?p2 =>
      make_compatible_light ltac:(fun _ =>
        match goal with
        | [ |- prv _ _ ] => apply intro_and_destruct
        | [ |- tprv _ _ ] => apply intro_and_destruct_T
        end
      );
      fintro_pat' p1; fintro_pat' p2
  | patOr ?p1 ?p2 =>
      make_compatible_light ltac:(fun _ =>
        match goal with
        | [ |- prv _ _ ] => apply intro_or_destruct
        | [ |- tprv _ _ ] => apply intro_or_destruct_T
        end
      );
      [fintro_pat' p1 | fintro_pat' p2]
  | patId ?id =>
      match goal with
      | [ |- ?A ⊢ ∀ ?t ] => let x := varname_from_pat pat in fintro_ident x
      | [ |- ?A ⊩ ∀ ?t ] => let x := varname_from_pat pat in fintro_ident x
      | [ |- ?A ⊢ (?s → ?t) ] => apply II
      | [ |- ?A ⊩ (?s → ?t) ] => apply II
      
      | [ |- @pm _ _ _ ?p ?C (named_quant All _ ?t) ] => let x := varname_from_pat pat in fintro_ident x
      | [ |- @pm _ _ _ ?p ?C (quant All ?t) ] => let x := varname_from_pat pat in fintro_ident x
      | [ |- @tpm _ _ _ ?p ?C (named_quant All _ ?t) ] => let x := varname_from_pat pat in fintro_ident x
      | [ |- @tpm _ _ _ ?p ?C (quant All ?t) ] => let x := varname_from_pat pat in fintro_ident x
      | [ |- @pm _ _ _ ?p ?C (?s → ?t) ] => apply II; let name := hypname_from_pattern C id in change (@pm _ _ _ p (ccons name s C) t)
      | [ |- @tpm _ _ _ ?p ?C (?s → ?t) ] => apply II; let name := hypname_from_pattern C id in change (@tpm _ _ _ p (tcons name s C) t)
      | _ =>
        
        progress custom_unfold; simpl_subst; try update_binder_names;
        custom_unfold;
        fintro_pat' pat;
        custom_fold
      end
  | patRewrite => fintro_pat' constr:(patId "?"); make_compatible ltac:(frewrite' 0 ([] : list form) false)
  | patRewriteBack => fintro_pat' constr:(patId "?"); make_compatible ltac:(frewrite' 0 ([] : list form) true)
  end.

Ltac fintro_pat intro_pat :=
  let pat := match intro_pat with
    | "..." => match get_form_goal with ?t → _ => create_deep_pattern t end
    | _ => match eval cbn in (parse_intro_pattern intro_pat) with
            | Some ?p => p
            | None => let msg := eval cbn in ("Invalid intro pattern: " ++ intro_pat) in fail 2 msg
            | ?q => idtac "AAA" q
            end
  end in fintro_pat' pat.

Tactic Notation "fintro" := fintro_pat constr:("?").
Tactic Notation "fintro" constr(H) := fintro_pat H.
Tactic Notation "fintro" ident(x) := fintro_ident x.

Tactic Notation "fintros" := repeat fintro.

Tactic Notation "fintros" constr(H1) := fintro_pat H1.
Tactic Notation "fintros" ident(H1) := fintro_ident H1.

Tactic Notation "fintros" constr(H1) constr(H2) := fintro_pat H1; fintro_pat H2.
Tactic Notation "fintros" ident(H1) constr(H2) := fintro_ident H1; fintro_pat H2.
Tactic Notation "fintros" constr(H1) ident(H2) := fintro_pat H1; fintro_ident H2.
Tactic Notation "fintros" ident(H1) ident(H2) := fintro_ident H1; fintro_ident H2.

Tactic Notation "fintros" constr(H1) constr(H2) constr(H3) := fintro_pat H1; fintro_pat H2; fintro_pat H3.
Tactic Notation "fintros" ident(H1) constr(H2) constr(H3) := fintro_ident H1; fintro_pat H2; fintro_pat H3.
Tactic Notation "fintros" constr(H1) ident(H2) constr(H3) := fintro_pat H1; fintro_ident H2; fintro_pat H3.
Tactic Notation "fintros" constr(H1) constr(H2) ident(H3) := fintro_pat H1; fintro_pat H2; fintro_ident H3.
Tactic Notation "fintros" ident(H1) ident(H2) constr(H3) := fintro_ident H1; fintro_ident H2; fintro_pat H3.
Tactic Notation "fintros" constr(H1) ident(H2) ident(H3) := fintro_pat H1; fintro_ident H2; fintro_ident H3.
Tactic Notation "fintros" ident(H1) ident(H2) ident(H3) := fintro_ident H1; fintro_ident H2; fintro_ident H3.

Tactic Notation "fintros" constr(H1) constr(H2) constr(H3) constr(H4) := fintro_pat H1; fintro_pat H2; fintro_pat H3; fintro_pat H4.
Tactic Notation "fintros" constr(H1) constr(H2) constr(H3) constr(H4) constr(H5) := fintro_pat H1; fintro_pat H2; fintro_pat H3; fintro_pat H4; fintro_pat H4.


Ltac is_hyp H := match type of H with ?t => match type of t with Prop => idtac end end.

Ltac turn_into_hypothesis T H contxt :=
  tryif is_hyp T
  then assert (H := T)
  else match goal with
  | [ |- @prv _ _ _ ?p ?C _ ] =>
      match type of T with
      | form => assert (@prv _ _ _ p C T) as H by ctx
      | nat => let T' := nth C T in assert (@prv _ _ _ p C T') as H by ctx
      | string => match lookup contxt T with
        | @None => let msg := eval cbn in ("Unknown identifier: " ++ T) in fail 4 msg
        | @Some _ ?n => let T' := nth C n in assert (@prv _ _ _ p C T') as H by ctx
        end
      end
  | [ |- @tprv _ _ _ ?p ?C _ ] =>
      match type of T with
      | form => assert (@tprv _ _ _ p C T) as H by ctx
      | nat => let T' := nth C T in assert (@tprv _ _ _ p C T') as H by ctx
      | string => match lookup contxt T with
        | @None => let msg := eval cbn in ("Unknown identifier: " ++ T) in fail 4 msg
        | @Some _ ?n => let T' := nth C n in assert (@tprv _ _ _ p C T') as H by ctx
        end
      end
  end.

Section ContextUtil.
  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.
  Context {ff : falsity_flag}.
  Variable p : peirce.

  Fixpoint replace C n (phi : form) :=
    match n, C with
      | 0, _::C => phi :: C
      | S n, x::C => x :: replace C n phi
      | _, _ => C
    end.

  Lemma replace_incl C n phi :
    incl (replace C n phi) (phi::C).
  Proof.
    revert C. induction n; destruct C; cbn; firstorder.
  Qed.
End ContextUtil.

Ltac fix_context_names C_named C_raw :=
  match C_named with
  | cnil => constr:(cnil)
  | tnil => constr:(tnil)
  | tblackbox _ => match C_raw with tblackbox ?C => C_raw | _ => constr:(tblackbox C_raw) end
  | cblackbox _ => match C_raw with cblackbox ?C => C_raw | _ => constr:(cblackbox C_raw) end
  | ccons ?s _ ?A => match C_raw with ?x::?B => let B' := fix_context_names A B in constr:(ccons s x B') end
  | tcons ?s _ ?A => match C_raw with extend ?x ?B => let B' := fix_context_names A B in constr:(tcons s x B') end
  | _ => C_raw
  end.

Ltac replace_context T_old H_new :=
  let C := get_context_goal in
  let phi := get_form_hyp H_new in
  let psi := get_form_goal in
  let X := fresh in
  (enough_compat (phi → psi) as X by eapply (IE X); apply H_new);
  let C' := match type of T_old with
    | nat => constr:(replace C T_old phi)
    
    | string => match lookup C T_old with
      | @None => let msg := eval cbn in ("Unknown identifier: " ++ T_old) in fail 4 msg
      | @Some _ ?n => constr:(replace C n phi)
      end
  end in
  fintro; apply (Weak (A := C')); [ | apply replace_incl];
  let C' := eval cbn [replace ccons tcons cnil tnil] in C' in
  match goal with
  | [ |- @pm _ _ _ ?p _ _ ] => let C' := fix_context_names C C' in change (@pm _ _ _ p C' psi)
  | [ |- @tpm _ _ _ ?p _ _ ] => let C' := fix_context_names C C' in change (@tpm _ _ _ p C' psi)
  | _ => idtac
  end.


Ltac fspecialize_list H A :=
  match A with
  | [] => simpl_subst H
  | ?x::?A' =>
      
      tryif (
        let H' := fresh "H" in
        make_compatible ltac:(fun C => turn_into_hypothesis x H' C);
        apply (fun H => IE H H') in H;
        clear H'
      ) then idtac
      else (
        
        let x' := fresh "x" in
        eapply (AllE ?[x']) in H;
        instantiate (x' := x)
      );
      fspecialize_list H A'
  end.

Ltac fspecialize_context T A :=
  
  match A with
  | [] => idtac
  | _ =>
      let H := fresh "H" in
      make_compatible_light ltac:(fun C => turn_into_hypothesis T H C);
      fspecialize_list H A;
      replace_context T H;
      try update_binder_names;
      try simpl_subst;
      clear H
  end.

Ltac fspecialize' T A := tryif is_hyp T then fspecialize_list T A else fspecialize_context T A.

Tactic Notation "fspecialize" "(" constr(H) constr(x1) ")" := fspecialize' H constr:([x1]).
Tactic Notation "fspecialize" "(" constr(H) constr(x1) constr(x2) ")" := fspecialize' H constr:([x1; x2]).
Tactic Notation "fspecialize" "(" constr(H) constr(x1) constr(x2) constr(x3) ")" := fspecialize' H constr:([x1;x2;x3]).

Tactic Notation "fspecialize" constr(H) "with" constr(x1) := fspecialize' H constr:([x1]).
Tactic Notation "fspecialize" constr(H) "with" constr(x1) constr(x2) := fspecialize' H constr:([x1;x2]).
Tactic Notation "fspecialize" constr(H) "with" constr(x1) constr(x2) constr(x3) := fspecialize' H constr:([x1;x2;x3]).


Section Fapply.
  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.
  Context {ff : falsity_flag}.
  Variable p : peirce.

  Lemma fapply_equiv_l A phi psi :
    A ⊢ (phi ↔ psi) -> A ⊢ phi -> A ⊢ psi.
  Proof.
    intros. apply (IE (phi := phi)). eapply CE1. apply H. apply H0.
  Qed.

  Lemma fapply_equiv_r A phi psi :
    A ⊢ (phi ↔ psi) -> A ⊢ psi -> A ⊢ phi.
  Proof.
    intros. apply (IE (phi := psi)). eapply CE2. apply H. apply H0.
  Qed.

  Context {eq_dec_Funcs : eq_dec syms}.
  Context {eq_dec_Preds : eq_dec preds}.

  Lemma fapply_equiv_l_T A phi psi :
    A ⊩ (phi ↔ psi) -> A ⊩ phi -> A ⊩ psi.
  Proof.
    intros. apply (IE (phi := phi)). eapply CE1. apply H. apply H0.
  Qed.

  Lemma fapply_equiv_r_T A phi psi :
    A ⊩ (phi ↔ psi) -> A ⊩ psi -> A ⊩ phi.
  Proof.
    intros. apply (IE (phi := psi)). eapply CE2. apply H. apply H0.
  Qed.
End Fapply.


Ltac fapply_without_quant H :=
  tryif exact H then idtac else
  let Hs := fresh "Hs" in
  let Ht := fresh "Ht" in
  match get_form_hyp H with
  | ?s → ?t =>
    match goal with
    | [ |- @prv _ _ _ ?p ?A _ ] =>
        enough (@prv _ _ _ p A s) as Hs;
        [ assert (@prv _ _ _ p A t) as Ht;
          [ eapply (IE H Hs) | fapply_without_quant Ht; clear Hs; clear Ht ]
        | ]
    | [ |- @tprv _ _ _ ?p ?A _ ] =>
        enough (@tprv _ _ _ p A s) as Hs;
        [ assert (@tprv _ _ _ p A t) as Ht;
          [ apply (IE H Hs) | fapply_without_quant Ht; clear Hs; clear Ht ]
        | ]
    end
  
  
  | _ ↔ _ =>
    match goal with
    | [ |- prv _ _] => tryif apply (fapply_equiv_l H) then idtac else apply (fapply_equiv_r H)
    | [ |- tprv _ _] => tryif apply (fapply_equiv_l_T H) then idtac else apply (fapply_equiv_r_T H)
    end
  
  
  | ∀ _ => eapply AllE in H; simpl_subst H; fapply_without_quant H

  
  | _ =>
    progress custom_unfold; simpl_subst H;
    custom_unfold;
    fapply_without_quant H;
    custom_fold
  end.

Ltac instantiate_evars H := repeat eassert (H := H _); repeat eapply AllE in H.

Ltac assert_premises H :=
  match type of H with
  | ?A -> ?B =>
      let H' := fresh "H" in assert A as H';
      [|specialize (H H'); clear H'; assert_premises H ]
  | forall _, _ => eassert (H := H _); assert_premises H
  | _ => idtac
  end.

Ltac feapply' T A := fun contxt =>
  let H := fresh "H" in
  turn_into_hypothesis T H contxt;
  
  assert_premises H;
  
  try (
    fspecialize_list H A;
    instantiate_evars H;
    simpl_subst H;
    let C := get_context_goal in
    eapply (Weak (B := C)) in H; [| solve_list_incl];
    fapply_without_quant H;
    
    revgoals;
    custom_fold
  );
  clear H.

Ltac fapply' T A contxt :=
  let H := fresh "H" in
  turn_into_hypothesis T H contxt;
  
  assert_premises H;
  
  try (
    fspecialize_list H A;
    instantiate_evars H;
    simpl_subst H;
    let C := get_context_goal in
    eapply (Weak (B := C)) in H; [| solve_list_incl];
    fapply_without_quant H;
    
    revgoals;
    custom_fold;
    
    
    tryif has_evar ltac:(type of H)
    then fail 3 "Cannot find instance for variable. Try feapply?"
    else clear H
  );
  try clear H.

Tactic Notation "feapply" constr(T) := make_compatible ltac:(feapply' T constr:([] : list form)).
Tactic Notation "feapply" "(" constr(T) constr(x1) ")" := make_compatible ltac:(feapply' T constr:([x1])).
Tactic Notation "feapply" "(" constr(T) constr(x1) constr(x2) ")" := make_compatible ltac:(feapply' T constr:([x1;x2])).
Tactic Notation "feapply" "(" constr(T) constr(x1) constr(x2) constr(x3) ")" := make_compatible ltac:(feapply' T constr:([x1;x2;x3])).

Tactic Notation "fapply" constr(T) := make_compatible ltac:(fapply' T constr:([] : list form)).
Tactic Notation "fapply" "(" constr(T) constr(x1) ")" := make_compatible ltac:(fapply' T constr:([x1])).
Tactic Notation "fapply" "(" constr(T) constr(x1) constr(x2) ")" := make_compatible ltac:(fapply' T constr:([x1;x2])).
Tactic Notation "fapply" "(" constr(T) constr(x1) constr(x2) constr(x3) ")" := make_compatible ltac:(fapply' T constr:([x1;x2;x3])).

Tactic Notation "feapply_light" constr(T) := make_compatible_light ltac:(feapply' T constr:([] : list form)).

Tactic Notation "feapply" "(" constr(T) ")" := make_compatible ltac:(feapply' T constr:([] : list form)).
Tactic Notation "fapply" "(" constr(T) ")" := make_compatible ltac:(fapply' T constr:([] : list form)).


Ltac fapply_in_without_quant_in T_hyp H_imp H_hyp :=
  match get_form_hyp H_imp with
  | ?s → ?t =>
    let H_hyp' := fresh "H_hyp'" in
    tryif assert_compat t as H_hyp' by (feapply_light H_imp; apply H_hyp)
    then (replace_context T_hyp H_hyp'; clear H_hyp')
    else (
      
      let Hs := fresh "Hs" in
      let Ht := fresh "Ht" in
      (enough_compat s as Hs); [
        (assert_compat t as Ht by apply (IE H_imp Hs));
        
        fapply_in_without_quant_in T_hyp Ht H_hyp;
        clear Ht; clear Hs
      | ] )
  
  
  | ?s ↔ ?t =>
    let H_hyp' := fresh "H_hyp'" in
    (tryif assert_compat t as H_hyp' by (feapply_light H_imp; apply H_hyp) then idtac
    else assert_compat s as H_hyp' by (feapply_light H_imp; apply H_hyp));
    replace_context T_hyp H_hyp'; clear H_hyp'
  
  
  | ∀ _ => instantiate_evars H_imp; fapply_in_without_quant_in T_hyp H_imp H_hyp

  
  | _ =>
    progress custom_unfold; simpl_subst H_imp; simpl_subst H_hyp;
    custom_unfold;
    fapply_in_without_quant_in T_hyp H_imp H_hyp;
    custom_fold
  end.

Ltac feapply_in T_imp A T_hyp :=
  let H_imp := fresh "H_imp" in
  let H_hyp := fresh "H_hyp" in
  make_compatible ltac:(fun contxt =>
    turn_into_hypothesis T_imp H_imp contxt;
    turn_into_hypothesis T_hyp H_hyp contxt
  );
  
  assert_premises H_imp;
  
  try (
    let C := get_context_goal in
    fspecialize_list H_imp A;
    instantiate_evars H_imp;
    simpl_subst H_imp;
    eapply (Weak (B := C)) in H_imp; [| solve_list_incl];
    fapply_in_without_quant_in T_hyp H_imp H_hyp;
    
    revgoals;
    simpl_subst;
    try update_binder_names;
    clear H_imp; clear H_hyp
  ).

Ltac fapply_in T_imp A T_hyp :=
  feapply_in T_imp A T_hyp;
  
  
  let C := get_context_goal in
  let phi := get_form_goal in
  tryif has_evar C then fail 3 "Cannot find instance for variable. Try feapply?"
  else tryif has_evar phi then fail 3 "Cannot find instance for variable. Try feapply?"
  else idtac.

Tactic Notation "feapply" constr(T_imp) "in" constr(T_hyp) := feapply_in T_imp constr:([] : list form) T_hyp.
Tactic Notation "feapply" "(" constr(T_imp) constr(x1) ")" "in" constr(T_hyp) := feapply_in T_imp constr:([x1] : list form) T_hyp.
Tactic Notation "feapply" "(" constr(T_imp) constr(x1) constr(x2) ")" "in" constr(T_hyp) := feapply_in T_imp constr:([x1;x2] : list form) T_hyp.
Tactic Notation "feapply" "(" constr(T_imp) constr(x1) constr(x2) constr(x3) ")" constr(T_hyp) := feapply_in T_imp constr:([x1;x2;x3] : list form) T_hyp.

Tactic Notation "fapply" constr(T_imp) "in" constr(T_hyp) := fapply_in T_imp constr:([] : list form) T_hyp.
Tactic Notation "fapply" "(" constr(T_imp) constr(x1) ")" "in" constr(T_hyp) := fapply_in T_imp constr:([x1] : list form) T_hyp.
Tactic Notation "fapply" "(" constr(T_imp) constr(x1) constr(x2) ")" "in" constr(T_hyp) := fapply_in T_imp constr:([x1;x2] : list form) T_hyp.
Tactic Notation "fapply" "(" constr(T_imp) constr(x1) constr(x2) constr(x3) ")" constr(T_hyp) := fapply_in T_imp constr:([x1;x2;x3] : list form) T_hyp.


Section Fassert.
  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.
  Context {ff : falsity_flag}.

  Lemma fassert_help `{peirce} A phi psi :
    A ⊢ phi -> A ⊢ (phi → psi) -> A ⊢ psi.
  Proof.
    intros H1 H2. eapply IE. exact H2. exact H1.
  Qed.

  Context {eq_dec_Funcs : eq_dec syms}.
  Context {eq_dec_Preds : eq_dec preds}.

  Lemma fassert_help_T `{peirce} A phi psi :
    A ⊩ phi -> A ⊩ (phi → psi) -> A ⊩ psi.
  Proof.
    intros H1 H2. eapply IE. exact H2. exact H1.
  Qed.
End Fassert.

Ltac fassert' phi := fun _ =>
  let H1 := fresh "H" in
  let H2 := fresh "H" in
  match goal with
  | [ |- prv ?A ?psi ] =>
    assert (A ⊢ phi) as H1; [ |
      assert (A ⊢ (phi → psi)) as H2; [ clear H1 |
        apply (fassert_help H1 H2)
      ]
    ]
  | [ |- ?A ⊩ ?psi ] =>
    assert (A ⊩ phi) as H1; [ |
      assert (A ⊩ (phi → psi)) as H2; [ clear H1 |
        apply (fassert_help_T H1 H2)
      ]
    ]
  end.

Tactic Notation "fassert" constr(phi) := (make_compatible ltac:(fassert' phi)); [| fintro].
Tactic Notation "fassert" constr(phi) "as" constr(H) := (make_compatible ltac:(fassert' phi)); [| fintro_pat H].
Tactic Notation "fassert" constr(phi) "by" tactic(tac) := (make_compatible ltac:(fassert' phi)); [tac | fintro].
Tactic Notation "fassert" constr(phi) "as" constr(H) "by" tactic(tac) := (make_compatible ltac:(fassert' phi)); [tac | fintro_pat H].



Section Fdestruct.
  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.
  Context {ff : falsity_flag}.
  Context {p : peirce}.

  Fixpoint remove_n (C : list form) n :=
    match n, C with
    | 0, x::C => C
    | S n, x::C => x::remove_n C n
    | _, _ => C
    end.

  Definition move_to_front C n :=
    match nth_error C n with
      | Some x => x :: remove_n C n
      | None => C
    end.

  Lemma remove_n_incl C n :
    incl (remove_n C n) C.
  Proof.
    revert C. induction n; destruct C; firstorder.
  Qed.

  Lemma move_to_front_incl C n :
    incl (move_to_front C n) C.
  Proof.
    unfold move_to_front. destruct nth_error eqn:H. 2: easy. intros x [->|].
    - eapply nth_error_In, H.
    - eapply remove_n_incl, H0.
  Qed.

  Lemma fdestruct_discharge_premises T a b c :
    T ⊢ a -> T ⊢ b → c -> T ⊢ (a → b) → c.
  Proof.
    intros H1 H2. fintros. fapply H2. fapply 0. eapply Weak. apply H1. firstorder.
  Qed.

  Context {eq_dec_Funcs : eq_dec syms}.
  Context {eq_dec_Preds : eq_dec preds}.

  Lemma fdestruct_discharge_premises_T T a b c :
    T ⊩ a -> T ⊩ (b → c) -> T ⊩ ((a → b) → c).
  Proof.
    intros H1 H2. fintros. fapply H2. fapply 0. eapply Weak. apply H1. firstorder.
  Qed.
End Fdestruct.

Ltac frevert T :=
  let C := get_context_goal in
  let n := match type of T with
    | nat => T
    | string => match lookup C T with
      | @None => let msg := eval cbn in ("Unknown identifier: " ++ T) in fail 4 msg
      | @Some _ ?n => n
      end
  end in
  let phi := nth C n in
  let C' := constr:(move_to_front C n) in
  apply (Weak (A := C')); [| apply move_to_front_incl];
  cbn [move_to_front remove_n nth_error ccons tcons cnil tnil];
  match goal with
  | [ |- prv ?C' ?psi ] => apply -> imps
  | [ |- tprv ?C' ?psi ] => apply -> switch_imp_T
  | [ |- pm ?C' ?psi ] =>
      apply -> imps;
      let C' := get_context_goal in
      let C'_named := remove C n in
      let C' := fix_context_names C'_named C' in
      change (pm C' (phi → psi))
  | [ |- tpm ?C' ?psi ] =>
      apply -> switch_imp_T;
      let C' := get_context_goal in
      let C'_named := remove C n in
      let C' := fix_context_names C'_named C' in
      change (tpm C' (phi → psi))
  end.

Ltac fdestruct_discharge_premises :=
  try (
    match goal with
    | [ |- prv _ _ ] => apply fdestruct_discharge_premises
    | [ |- tprv _ _ ] => apply fdestruct_discharge_premises_T
    | [ |- pm _ _ ] => make_compatible ltac:(fun _ => apply fdestruct_discharge_premises)
    | [ |- tpm _ _ ] => make_compatible ltac:(fun _ => apply fdestruct_discharge_premises_T)
    end;
    [| fdestruct_discharge_premises ]).

Ltac fdestruct' T A pat :=
  tryif is_hyp T then (
    
    let H := fresh "H" in
    let X := fresh "X" in
    assert (H := T);
    let s := get_form_hyp H in
    match goal with
    | [ |- prv ?C ?t ] => enough (C ⊢ (s → t)) as X by (feapply X; feapply H)
    | [ |- tprv ?C ?t ] => enough (C ⊩ (s → t)) as X by (feapply X; feapply H)
    | [ |- pm ?C ?t ] => enough (pm C (s → t)) as X by (feapply X; feapply H)
    | [ |- tpm ?C ?t ] => enough (tpm C (s → t)) as X by (feapply X; feapply H)
    end;
    fintro "?"; fdestruct' 0 A pat; clear H
  )
  else (
    try fspecialize_context T A;
    frevert T;
    
    fdestruct_discharge_premises;
    
    try (let pattern := lazymatch pat with
    | "" => match get_form_goal with ?t → _ => create_pattern t end
    | "..." => match get_form_goal with ?t → _ => create_deep_pattern t end
    | _ =>
      match eval cbn in (parse_intro_pattern pat) with
      | @Some _ ?p => p
      | @None => let msg := eval cbn in ("Invalid pattern: " ++ pat) in fail 3 msg
      end
    end in
    fintro_pat' pattern;
    try update_binder_names)
  ).

Tactic Notation "fdestruct" constr(T) := fdestruct' T constr:([] : list form) "".
Tactic Notation "fdestruct" "(" constr(T) constr(x1) ")" := fdestruct' T constr:([x1]) "".
Tactic Notation "fdestruct" "(" constr(T) constr(x1) constr(x2) ")" := fdestruct' T constr:([x1;x2]) "".
Tactic Notation "fdestruct" "(" constr(T) constr(x1) constr(x2) constr(x3) ")" := fdestruct' T constr:([x1;x2;x3]) "".

Tactic Notation "fdestruct" constr(T) "as" constr(pat) := fdestruct' T constr:([] : list form) pat.
Tactic Notation "fdestruct" "(" constr(T) constr(x1) ")" "as" constr(pat) := fdestruct' T constr:([x1]) pat.
Tactic Notation "fdestruct" "(" constr(T) constr(x1) constr(x2) ")" "as" constr(pat) := fdestruct' T constr:([x1;x2]) pat.
Tactic Notation "fdestruct" "(" constr(T) constr(x1) constr(x2) constr(x3) ")" "as" constr(pat) := fdestruct' T constr:([x1;x2;x3]) pat.

Tactic Notation "feapply" constr(T_imp) "in" constr(T_hyp) "as" constr(pat) := feapply_in T_imp constr:([] : list form) T_hyp; try fdestruct T_hyp as pat.
Tactic Notation "feapply" "(" constr(T_imp) constr(x1) ")" "in" constr(T_hyp) "as" constr(pat) := feapply_in T_imp constr:([x1] : list form) T_hyp; try fdestruct T_hyp as pat.
Tactic Notation "feapply" "(" constr(T_imp) constr(x1) constr(x2) ")" "in" constr(T_hyp) "as" constr(pat) := feapply_in T_imp constr:([x1;x2] : list form) T_hyp; try fdestruct T_hyp as pat.
Tactic Notation "feapply" "(" constr(T_imp) constr(x1) constr(x2) constr(x3) ")" constr(T_hyp) "as" constr(pat) := feapply_in T_imp constr:([x1;x2;x3] : list form) T_hyp; try fdestruct T_hyp as pat.

Tactic Notation "fapply" constr(T_imp) "in" constr(T_hyp) "as" constr(pat) := fapply_in T_imp constr:([] : list form) T_hyp; try fdestruct T_hyp as pat.
Tactic Notation "fapply" "(" constr(T_imp) constr(x1) ")" "in" constr(T_hyp) "as" constr(pat) := fapply_in T_imp constr:([x1] : list form) T_hyp; try fdestruct T_hyp as pat.
Tactic Notation "fapply" "(" constr(T_imp) constr(x1) constr(x2) ")" "in" constr(T_hyp) "as" constr(pat) := fapply_in T_imp constr:([x1;x2] : list form) T_hyp; try fdestruct T_hyp as pat.
Tactic Notation "fapply" "(" constr(T_imp) constr(x1) constr(x2) constr(x3) ")" constr(T_hyp) "as" constr(pat) := fapply_in T_imp constr:([x1;x2;x3] : list form) T_hyp; try fdestruct T_hyp as pat.


Section Classical.
  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.

  Lemma case_help A phi psi :
    A ⊢C (phi ∨ (phi → ⊥) → psi) -> A ⊢C psi.
  Proof.
    intro H. eapply IE. apply H.
    eapply IE. eapply Pc.
    apply II. apply DI2. apply II.
    eapply IE. apply Ctx. right. now left.
    apply DI1. apply Ctx. now left.
  Qed.

  Lemma contradiction_help A phi :
    A ⊢C ((phi → ⊥) → ⊥) -> A ⊢C phi.
  Proof.
    intro H. eapply IE. eapply Pc. apply II.
    apply Exp. eapply IE. eapply Weak. apply H. firstorder.
    apply II. eapply IE. apply Ctx. right. now left.
    apply Ctx. now left.
  Qed.

  Context {eq_dec_Funcs : eq_dec syms}.
  Context {eq_dec_Preds : eq_dec preds}.

  Lemma case_help_T A phi psi :
    A ⊩C (phi ∨ (phi → ⊥) → psi) -> A ⊩C psi.
  Proof.
    intro H. eapply IE. apply H.
    eapply IE. eapply Pc.
    apply II. apply DI2. apply II.
    eapply IE. apply Ctx. firstorder.
    apply DI1. apply Ctx. firstorder.
  Qed.

  Lemma contradiction_help_T A phi :
    A ⊩C ((phi → ⊥) → ⊥) -> A ⊩C phi.
  Proof.
    intro H. eapply IE. eapply Pc. apply II.
    apply Exp. eapply IE. eapply Weak. apply H. firstorder.
    apply II. eapply IE. apply Ctx. firstorder.
    apply Ctx. firstorder.
  Qed.

End Classical.

Tactic Notation "fclassical" constr(phi) "as" constr(H1) constr(H2) :=
  make_compatible ltac:(fun _ =>
    match goal with
    | [ |- prv _ _ ] => apply (case_help (phi := phi))
    | [ |- tprv _ _ ] => apply (case_help_T (phi := phi))
    end
  ); let pat := eval cbn in ("[" ++ H1 ++ "|" ++ H2 ++ "]") in fintro_pat pat.
Tactic Notation "fclassical" constr(phi) "as" constr(H) := fclassical phi as H H.
Tactic Notation "fclassical" constr(phi) := fclassical phi as "".

Tactic Notation "fcontradict" "as" constr(H) :=
  make_compatible ltac:(fun _ =>
    match goal with
    | [ |- _ ⊢ _ ] => apply contradiction_help
    | [ |- _ ⊩ _ ] => apply contradiction_help_T
    end
  ); fintro_pat H.
Tactic Notation "fcontradict" := fcontradict as "?".


Definition cast {X} {x y: X} {p: X -> Type}
  : x = y -> p x -> p y
  := fun e a => match e with eq_refl => a end.

Fixpoint VecForall2 {X Y n} (p : X -> Y -> Prop) (v1 : Vector.t X n) (v2 : Vector.t Y n) :=
  match v1 in Vector.t _ n return Vector.t Y n -> Prop with
  | @Vector.nil _ => fun _ => True
  | @Vector.cons _ x _ v1 => fun v2 => p x (Vector.hd v2) /\ VecForall2 p v1 (Vector.tl v2)
  end v2.

Class Leibniz (Σ_funcs : funcs_signature) (Σ_preds : preds_signature) (ff : falsity_flag) :=
{
  Eq_pred : preds ;
  eq_binary : 2 = ar_preds Eq_pred ;
  eq s t := @atom Σ_funcs Σ_preds _ _ Eq_pred (cast eq_binary (Vector.cons term s 1 (Vector.cons term t 0 (Vector.nil term)))) ;

  Axioms : list form ;

  eq_refl `{peirce} : Axioms ⊢ ∀ (eq ($0) ($0)) ;
  eq_sym `{peirce} : Axioms ⊢ ∀ ∀ (eq ($0) ($1) → eq ($1) ($0)) ;

  eq_func_congr `{peirce} : forall A F v1 v2, incl Axioms A -> VecForall2 (fun t1 t2 => A ⊢ eq t1 t2) v1 v2 -> A ⊢ eq (func F v1) (func F v2) ;
  eq_pred_congr `{peirce} : forall A P v1 v2, incl Axioms A -> VecForall2 (fun t1 t2 => A ⊢ eq t1 t2) v1 v2 -> A ⊢ atom P v1 <-> A ⊢ atom P v2 ;
}.

Lemma eq_subst_help `{funcs_signature} f y (v : Vector.t term 2) (e : 2 = y) :
  Vector.map f (cast e v) = cast e (@Vector.map term term f _ v).
Proof.
  destruct e. reflexivity.
Qed.

Lemma refl `{L : Leibniz, p : peirce} A x :
  incl Axioms A -> A ⊢ eq x x.
Proof.
  intros H. assert (H_refl := eq_refl). fspecialize (H_refl x).
  rewrite eq_subst_help in H_refl. eapply Weak. apply H_refl. easy.
Qed.

Lemma sym `{L : Leibniz, p : peirce} A x y :
  incl Axioms A -> A ⊢ eq x y -> A ⊢ eq y x.
Proof.
  intros H1 H2. assert (H_sym := eq_sym). fspecialize (H_sym y x).
  rewrite ! eq_subst_help in H_sym. simpl_subst H_sym. eapply IE. eapply Weak.
  apply H_sym. easy. easy.
Qed.

Lemma leibniz_term `{L : Leibniz} `{p : peirce} A t s1 s2 :
  incl Axioms A -> (forall n, A ⊢ eq (s1 n) (s2 n)) -> A ⊢ eq (t`[s1]) (t`[s2]).
Proof.
  intros HA H. induction t; cbn.
  - apply H.
  - apply eq_func_congr. easy. induction v; constructor. apply IH; left.
    apply IHv. intros. apply IH. now right.
Qed.

Lemma leibniz `{L : Leibniz} `{peirce} A phi t t' :
  incl Axioms A -> A ⊢ eq t t' -> A ⊢ phi[t..] -> A ⊢ phi[t'..].
Proof.
  enough (forall s1 s2, incl Axioms A ->(forall n, A ⊢ eq (s1 n) (s2 n)) -> A ⊢ phi[s1] <-> A ⊢ phi[s2]) as X.
  { intros. apply X with (s1 := t..). easy. intros []; cbn. easy. now apply refl. easy. }
  induction phi; intros s1 s2 HA H1.
  - easy.
  - cbn in *. eapply eq_pred_congr. easy. induction t0; constructor.
    now apply leibniz_term. apply IHt0.
  - cbn in *. destruct b0; split; intros H2.
    + apply CE in H2. fsplit. now apply (IHphi1 L A s1). now apply (IHphi2 L A s1).
    + apply CE in H2. fsplit. now apply (IHphi1 L A s1 s2). now apply (IHphi2 L A s1 s2).
    + eapply DE in H2. apply H2.
      * fleft. apply (IHphi1 L _ s1). now apply incl_tl. intros. eapply Weak.
        apply H1. now apply incl_tl. ctx.
      * fright. apply (IHphi2 L _ s1). now apply incl_tl. intros. eapply Weak.
        apply H1. now apply incl_tl. ctx.
    + eapply DE in H2. apply H2.
      * fleft. apply (IHphi1 L _ s1 s2). now apply incl_tl. intros. eapply Weak.
        apply H1. now apply incl_tl. ctx.
      * fright. apply (IHphi2 L _ s1 s2). now apply incl_tl. intros. eapply Weak.
        apply H1. now apply incl_tl. ctx.
    + fintros. apply (IHphi2 L _ s1 s2). now apply incl_tl. intros. eapply Weak.
      apply H1. now apply incl_tl. eapply IE. eapply Weak. apply H2. now apply incl_tl.
      apply (IHphi1 L _ s1 s2). now apply incl_tl. intros. eapply Weak.
      apply H1. apply incl_tl, incl_refl. ctx.
    + fintros. apply (IHphi2 L _ s1 s2). now apply incl_tl. intros. eapply Weak.
      apply H1. now apply incl_tl. eapply IE. eapply Weak. apply H2. now apply incl_tl.
      apply (IHphi1 L _ s1 s2). now apply incl_tl. intros. eapply Weak.
      apply H1. apply incl_tl, incl_refl. ctx.
  - destruct q; split; cbn; intros H2.
    + fintros. rewrite subst_comp. apply (IHphi L _ _ (up s1 >> subst_term x..)). easy.
      intros []; cbn. now apply refl. simpl_subst. simpl_subst. apply sym. easy. apply H1.
      rewrite <- subst_comp. now apply AllE.
    + fintros. rewrite subst_comp. apply (IHphi L _ _ (up s2 >> subst_term x..)). easy.
      intros []; cbn. now apply refl. simpl_subst. simpl_subst. apply H1.
      rewrite <- subst_comp. now apply AllE.
    + fdestruct H2. apply (ExI (t := x)). rewrite ! subst_comp.
      apply (IHphi L _ _ (up s1 >> subst_term x..)). now apply incl_tl. 2: ctx.
      intros []; cbn. apply refl; now apply incl_tl. simpl_subst. simpl_subst. apply sym. now apply incl_tl.
      eapply Weak. apply H1. now apply incl_tl.
    + fdestruct H2. apply (ExI (t := x)). rewrite ! subst_comp.
      apply (IHphi L _ _ (up s2 >> subst_term x..)). now apply incl_tl. 2: ctx.
      intros []; cbn. apply refl; now apply incl_tl. simpl_subst. simpl_subst.
      eapply Weak. apply H1. now apply incl_tl.
Qed.

Section FrewriteEquiv.
  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.
  Context {ff : falsity_flag}.
  Context {p : peirce}.

  Lemma frewrite_equiv_bin_l A op phi psi theta :
    A ⊢ (phi ↔ psi) -> A ⊢ (bin op phi theta ↔ bin op psi theta).
  Proof.
    intros E. fstart. destruct op; fsplit.
    - fintros "[P T]". fsplit. fapply E. ctx. ctx.
    - fintros "[P T]". fsplit. fapply E. ctx. ctx.
    - fintros "[P|T]". fleft. fapply E. ctx. fright. ctx.
    - fintros "[P|T]". fleft. fapply E. ctx. fright. ctx.
    - fintros "H" "P". fapply "H". fapply E. ctx.
    - fintros "H" "P". fapply "H". fapply E. ctx.
  Qed.

  Lemma frewrite_equiv_bin_r A op phi psi theta :
    A ⊢ (phi ↔ psi) -> A ⊢ (bin op theta phi ↔ bin op theta psi).
  Proof.
    intros E. fstart. destruct op; fsplit.
    - fintros "[P T]". fsplit. ctx. fapply E. ctx.
    - fintros "[P T]". fsplit. ctx. fapply E. ctx.
    - fintros "[P|T]". fleft. ctx. fright. fapply E. ctx.
    - fintros "[P|T]". fleft. ctx. fright. fapply E. ctx.
    - fintros "H" "P". fapply E. fapply "H". ctx.
    - fintros "H" "P". fapply E. fapply "H". ctx.
  Qed.

  Lemma frewrite_equiv_bin_lr A op phi psi theta chi :
    A ⊢ (phi ↔ psi) -> A ⊢ (theta ↔ chi) -> A ⊢ (bin op phi theta ↔ bin op psi chi).
  Proof.
    intros E1 E2. fstart. destruct op; fsplit.
    - fintros "[P T]". fsplit. fapply E1. ctx. fapply E2. ctx.
    - fintros "[P C]". fsplit. fapply E1. ctx. fapply E2. ctx.
    - fintros "[P|T]". fleft. fapply E1. ctx. fright. fapply E2. ctx.
    - fintros "[P|C]". fleft. fapply E1. ctx. fright. fapply E2. ctx.
    - fintros "H" "P". fapply E2. fapply "H". fapply E1. ctx.
    - fintros "H" "P". fapply E2. fapply "H". fapply E1. ctx.
  Qed.

  Lemma frewrite_equiv_quant A op phi psi :
    A ⊢ (phi ↔ psi) -> A ⊢ (quant op phi[↑] ↔ quant op psi[↑]).
  Proof.
    intros E. fstart. destruct op; fsplit.
    - fintros "H" x. fapply E. fapply ("H" $0).     - fintros "H" x. fapply E. fapply ("H" $0).
    - fintros "[x H]". apply ExI with (t := x); simpl_subst. fapply E. ctx.
    - fintros "[x H]". apply ExI with (t := x); simpl_subst. fapply E. ctx.
  Qed.

  Lemma frewrite_equiv_switch A phi psi :
    A ⊢ (phi ↔ psi) -> A ⊢ (psi ↔ phi).
  Proof.
    intros E. fdestruct E. fsplit; ctx.
  Qed.

  Context {eq_dec_Funcs : EqDec syms}.
  Context {eq_dec_Preds : EqDec preds}.

  Lemma frewrite_equiv_bin_l_T T op phi psi theta :
    T ⊩ (phi ↔ psi) -> T ⊩ (bin op phi theta ↔ bin op psi theta).
  Proof.
    intros [A [ ]]. exists A. split. easy. now apply frewrite_equiv_bin_l.
  Qed.

  Lemma frewrite_equiv_bin_r_T T op phi psi theta :
    T ⊩ (phi ↔ psi) -> T ⊩ (bin op theta phi ↔ bin op theta psi).
  Proof.
    intros [A [ ]]. exists A. split. easy. now apply frewrite_equiv_bin_r.
  Qed.

  Lemma frewrite_equiv_bin_lr_T T op phi psi theta chi :
    T ⊩ (phi ↔ psi) -> T ⊩ (theta ↔ chi) -> T ⊩ (bin op phi theta ↔ bin op psi chi).
  Proof.
    intros [A [ ]] [B [ ]]. exists (List.app A B). split.
    now apply contains_app. apply frewrite_equiv_bin_lr.
    eapply Weak. apply H0. now apply incl_appl.
    eapply Weak. apply H2. now apply incl_appr.
  Qed.

  Lemma frewrite_equiv_quant_T T op phi psi :
    T ⊩ (phi ↔ psi) -> T ⊩ (quant op phi[↑] ↔ quant op psi[↑]).
  Proof.
    intros [A [ ]]. exists A. split. easy. now apply frewrite_equiv_quant.
  Qed.

  Lemma frewrite_equiv_switch_T T phi psi :
    T ⊩ (phi ↔ psi) -> T ⊩ (psi ↔ phi).
  Proof.
    intros [A [ ]]. exists A. split. easy. now apply frewrite_equiv_switch.
  Qed.

End FrewriteEquiv.

Ltac contains phi f := match phi with f => idtac | context P [ f ] => idtac end.

Ltac frewrite_equiv_solve H phi psi :=
  match get_form_goal with
  | phi ↔ psi => apply H
  | bin ?op ?l ?r ↔ _ => (
      tryif contains l phi
      then (tryif contains r phi
        then apply_compat frewrite_equiv_bin_lr frewrite_equiv_bin_lr_T
        else apply_compat frewrite_equiv_bin_l frewrite_equiv_bin_l_T)
      else apply_compat frewrite_equiv_bin_r frewrite_equiv_bin_r_T
    );
    frewrite_equiv_solve H phi psi
  | quant _ _ _ ↔ _ =>
    apply_compat frewrite_equiv_quant frewrite_equiv_quant_T;
    frewrite_equiv_solve H phi psi
  end.

Ltac frewrite_replace_all phi t s :=
  match phi with
  | context C[t] => let phi' := context C[s] in frewrite_replace_all phi' t s
  | _ => phi
  end.

Fixpoint up_n `{funcs_signature} n sigma := match n with
| 0 => sigma
| S n' => up (up_n n' sigma)
end.

Ltac shift_n n t :=
  match n with
  | 0 => t
  | S ?n' => shift_n n' (t`[↑])
  end.

Ltac vector_map_ltac v f :=
  match v with
  | Vector.nil ?t => constr:(Vector.nil t)
  | @Vector.cons _ ?x _ ?v' =>
    let x' := f x in
    let v'' := vector_map_ltac v' f in
    constr:(@Vector.cons _ x' _ v'')
  end.

Ltac add_shifts' n t G :=
  let f := add_shifts' n t in
  let t_shifted := shift_n n t in
  match G with
  
  | t_shifted => constr:(($n)`[up_n n t..])
  | $(?m) => constr:(($m)`[up_n n ↑]`[up_n n t..])
  | func ?fu ?vec => let vec' := vector_map_ltac vec f in constr:(func fu vec')
  
  | falsity => constr:(falsity[up_n n ↑][up_n n t..])
  | atom ?P ?vec => let vec' := vector_map_ltac vec f in constr:(atom P vec')
  | bin ?op ?u ?v => let u' := f u in let v' := f v in constr:(bin op u' v')
  | quant ?op ?u => let u' := add_shifts' (S n) t u in constr:(quant op u')
  
  | ?u => match type of u with
      | form => constr:(u[up_n n ↑][up_n n t..])
      | term => constr:(u`[up_n n ↑]`[up_n n t..])
      end
  end.
Ltac add_shifts := add_shifts' 0.

Ltac remove_shifts G t :=
  match G with
  | context C[ ?s[up_n ?n ↑][up_n ?n t..] ] => let G' := context C[ s[up_n n ↑] ] in remove_shifts G' t
  | context C[ ?s`[up_n ?n ↑]`[up_n ?n t..] ] => let G' := context C[ s`[up_n n ↑] ] in remove_shifts G' t
  | context C[ ($ ?n)`[up_n ?n t..] ] => let G' := context C[ $n ] in remove_shifts G' t
  | _ => G
  end.

Ltac repeat_n n tac := match n with 0 => idtac | S ?n' => tac; repeat_n n' tac end.

Ltac frewrite' T A back ::= fun contxt =>
  let H := fresh "H" in
  turn_into_hypothesis T H contxt;
  fspecialize_list H A;
  instantiate_evars H;
  simpl_subst H;

  
  custom_unfold;

  
  repeat match goal with
  | [ |- context C[fun x => $(S x)] ] => let G := context C[↑] in change G
  end;

  match get_form_hyp H with
  
  | ?_phi ↔ ?_psi =>
    let phi := match back with true => _psi | false => _phi end in
    let psi := match back with true => _phi | false => _psi end in
    match back with true => apply_compat frewrite_equiv_switch frewrite_equiv_switch_T in H | _ => idtac end;

    let G := get_form_goal in
    let G' := frewrite_replace_all G phi psi in
    let E := fresh "E" in
    assert_compat (G ↔ G') as E;
    [ frewrite_equiv_solve H phi psi |];
    feapply E;
    clear E

  
  | atom ?p (@Vector.cons _ ?_t _ (@Vector.cons _ ?_t' _ (Vector.nil term))) =>
    
    assert (p = Eq_pred) as _ by reflexivity;

    let t := match back with true => _t' | false => _t end in
    let t' := match back with true => _t | false => _t' end in
    
    
    let C := get_context_goal in
    let G := get_form_goal in
    let X := fresh in
    let G' := add_shifts t G in
    match goal with
    | [ |- _ ⊢ _ ] => enough (C ⊢ G') as X
    | [ |- _ ⊩ _ ] => enough (C ⊩ G') as X
    end;
    [
      repeat match type of X with context K[ ?u`[up_n ?n ↑]`[up_n ?n t..] ] =>
        let R := fresh in
        
        assert (u`[up_n n ↑]`[up_n n t..] = u) as R; [
          rewrite subst_term_comp; apply subst_term_id;
          let a := fresh in intros a;
          (repeat_n n ltac:(try destruct a)); reflexivity |];
        rewrite R in X
      end;
      apply X
    |];
    
    
    match goal with
    | [ |- ?U ⊢ ?G ] => let G' := remove_shifts G t in change (U ⊢ G'[t..])
    | [ |- ?U ⊩ ?G ] => let G' := remove_shifts G t in change (U ⊩ G'[t..])
    end;

    
    let t'' := fresh "t" in
    match goal with
    | [ |- prv _ _ ] => eapply leibniz
    | [ |- tprv _ _ ] => fail "Rewrite not supported under theories"
    end;
    [
      
      try (repeat (try apply incl_refl; apply incl_tl));
      
      firstorder
    |
      match back with
      | false =>
          apply sym;
          [ try (repeat (try apply incl_refl; apply incl_tl)); firstorder
          | fapply H ]
      | true => apply H
      end
    | ];
    
    
    cbn -[up_n];
    
    
    

    
    repeat match goal with [ |- context C[up_n ?n ↑ ?a] ] =>
      let G' := context C[ ($a)[up_n n ↑] ] in change G'
    end;

    
    repeat match goal with
    | [ |- context C[up_n ?n (up ?s)]] => let G' := context C[up_n (S n) s] in change G'
    | [ |- context C[up ?s]] => let G' := context C[up_n 1 s] in change G'
    end;

    
    repeat match goal with [ |- context K[ ?u `[up_n ?n ↑]`[up_n ?n t'..] ]] =>
      let R := fresh in
      
      assert (u`[up_n n ↑]`[up_n n t'..] = u) as R; [
        rewrite subst_term_comp; apply subst_term_id;
        let a := fresh in intros a;
        (repeat_n n ltac:(try destruct a)); reflexivity |];
      rewrite ! R;
      clear R
    end;

    
    cbn; try rewrite !subst_shift; try rewrite !subst_term_shift;

    
    custom_fold;
    simpl_subst
  end;
  clear H.

Tactic Notation "frewrite" constr(T) := make_compatible ltac:(frewrite' T constr:([] : list form) constr:(false)).
Tactic Notation "frewrite" "(" constr(T) constr(x1) ")" := make_compatible ltac:(frewrite' T constr:([x1]) constr:(false)).
Tactic Notation "frewrite" "(" constr(T) constr(x1) constr(x2) ")" := make_compatible ltac:(frewrite' T constr:([x1;x2]) constr:(false)).
Tactic Notation "frewrite" "(" constr(T) constr(x1) constr(x2) constr(x3) ")" := make_compatible ltac:(frewrite' T constr:([x1;x2;x3]) constr:(false)).

Tactic Notation "frewrite" "<-" constr(T) := make_compatible ltac:(frewrite' T constr:([] : list form) constr:(true)).
Tactic Notation "frewrite" "<-" "(" constr(T) constr(x1) ")" := make_compatible ltac:(frewrite' T constr:([x1]) constr:(true)).
Tactic Notation "frewrite" "<-" "(" constr(T) constr(x1) constr(x2) ")" := make_compatible ltac:(frewrite' T constr:([x1;x2]) constr:(true)).
Tactic Notation "frewrite" "<-" "(" constr(T) constr(x1) constr(x2) constr(x3) ")" := make_compatible ltac:(frewrite' T constr:([x1;x2;x3]) constr:(true)).

Ltac fexists x := make_compatible ltac:(fun _ =>
  apply (ExI (t := x));
  simpl_subst).