FOcdint.FO_CDInt_Syntax
Require Import Lia.
Require Import Ensembles.
Require Import Coq.Vectors.Vector.
Local Notation vec := t.
From Equations Require Export Equations.
(* Some preliminary definitions for substitions *)
Definition scons {X: Type} (x : X) (xi : nat -> X) :=
fun n => match n with
| 0 => x
| S n => xi n
end.
Definition funcomp {X Y Z} (g : Y -> Z) (f : X -> Y) :=
fun x => g (f x).
(* Signatures are a record to allow for easier definitions of general transformations on signatures *)
Class funcs_signature :=
{ syms : Type; ar_syms : syms -> nat }.
Coercion syms : funcs_signature >-> Sortclass.
Class preds_signature :=
{ preds : Type; ar_preds : preds -> nat }.
Coercion preds : preds_signature >-> Sortclass.
Section fix_signature.
Context {Σ_funcs : funcs_signature}.
(* We use the stdlib definition of vectors to be maximally compatible *)
Unset Elimination Schemes.
Inductive term : Type :=
| var : nat -> term
| func : forall (f : syms), vec term (ar_syms f) -> term.
Set Elimination Schemes.
Fixpoint subst_term (σ : nat -> term) (t : term) : term :=
match t with
| var n => σ n
| func f v => func f (map (subst_term σ) v)
end.
Context {Σ_preds : preds_signature}.
(* Syntax is parametrised in binary operators and quantifiers.
Most developments will fix these types in the beginning and never change them.
*)
Class operators := {binop : Type ; quantop : Type}.
Context {ops : operators}.
Inductive form : Type :=
| bot : form
| atom : forall (P : preds), vec term (ar_preds P) -> form
| bin : binop -> form -> form -> form
| quant : quantop -> form -> form.
Definition up (σ : nat -> term) := scons (var 0) (funcomp (subst_term (funcomp var S)) σ).
Fixpoint subst_form (σ : nat -> term) (phi : form) : form :=
match phi with
| bot => bot
| atom P v => atom P (map (subst_term σ) v)
| bin op phi1 phi2 => bin op (subst_form σ phi1) (subst_form σ phi2)
| quant op phi => quant op (subst_form (up σ) phi)
end.
End fix_signature.
(* Setting implicit arguments is crucial *)
(* We can write term both with and without arguments, but printing is without. *)
Arguments term _, {_}.
Arguments var _ _, {_} _.
Arguments func _ _ _, {_} _ _.
Arguments subst_term {_} _ _.
(* Formulas can be written with the signatures explicit or not.
If the operations are explicit, the signatures are too.
*)
Arguments form _ _ _ , _ _ {_}, {_ _ _}.
Arguments atom _ _ _ , _ _ {_}, {_ _ _}.
Arguments bin _ _ _ , _ _ {_}, {_ _ _}.
Arguments quant _ _ _ , _ _ {_}, {_ _ _}.
Arguments up _, {_}.
Arguments subst_form _ _ _, _ _ {_}, {_ _ _}.
(* Substitution Notation *)
Declare Scope subst_scope.
Open Scope subst_scope.
Notation "$ x" := (var x) (at level 3, format "$ '/' x") : subst_scope.
Notation "t `[ sigma ]" := (subst_term sigma t) (at level 7, left associativity, format "t '/' `[ sigma ]") : subst_scope.
Notation "phi [ sigma ]" := (subst_form sigma phi) (at level 7, left associativity, format "phi '/' [ sigma ]") : subst_scope.
Notation "s .: sigma" := (scons s sigma) (at level 70, right associativity) : subst_scope.
Notation "f >> g" := (funcomp g f) (at level 50) : subst_scope.
Notation "s '..'" := (scons s var) (at level 4, format "s ..") : subst_scope.
Notation "↑" := (S >> var) : subst_scope.
(* Full syntax *)
Declare Scope syn.
Open Scope syn.
Module FullSyntax.
Inductive full_logic_sym : Type :=
| Conj : full_logic_sym
| Disj : full_logic_sym
| Impl : full_logic_sym.
Inductive full_logic_quant : Type :=
| All : full_logic_quant
| Ex : full_logic_quant.
Definition full_operators : operators :=
{| binop := full_logic_sym ; quantop := full_logic_quant |}.
#[export] Hint Immediate full_operators : typeclass_instances.
Notation "∀ Phi" := (@quant _ _ full_operators All Phi) (at level 50) : syn.
Notation "∃ Phi" := (@quant _ _ full_operators Ex Phi) (at level 50) : syn.
Notation "A ∧ B" := (@bin _ _ full_operators Conj A B) (at level 41) : syn.
Notation "A ∨ B" := (@bin _ _ full_operators Disj A B) (at level 42) : syn.
Notation "A '-->' B" := (@bin _ _ full_operators Impl A B) (at level 43, right associativity) : syn.
Notation "⊥" := (bot) : syn.
Notation "⊤" := (⊥ --> ⊥) : syn.
Notation "¬ A" := (A --> ⊥) (at level 42) : syn.
Notation "A '<-->' B" := ((A --> B) ∧ (B --> A)) (at level 43) : syn.
End FullSyntax.
Export FullSyntax.
Section fix_signature.
Context {Σ_funcs : funcs_signature}.
Context {Σ_preds : preds_signature}.
(* Example formula: *)
Compute (∀ ⊥ --> ⊥).
Context {ops : operators}.
(* Induction principle for terms *)
Inductive Forall {A : Type} (P : A -> Type) : forall {n}, t A n -> Type :=
| Forall_nil : Forall P (@Vector.nil A)
| Forall_cons : forall n (x : A) (l : t A n), P x -> Forall P l -> Forall P (@Vector.cons A x n l).
Inductive vec_in {A : Type} (a : A) : forall {n}, t A n -> Type :=
| vec_inB {n} (v : t A n) : vec_in a (cons A a n v)
| vec_inS a' {n} (v : t A n) : vec_in a v -> vec_in a (cons A a' n v).
Hint Constructors vec_in : core.
Lemma term_rect' (p : term -> Type) :
(forall x, p (var x)) -> (forall F v, (Forall p v) -> p (func F v)) -> forall (t : term), p t.
Proof.
intros f1 f2. fix strong_term_ind' 1. destruct t as [n | F v].
- apply f1.
- apply f2. induction v.
+ econstructor.
+ econstructor. now eapply strong_term_ind'. eauto.
Qed.
Lemma term_rect (p : term -> Type) :
(forall x, p (var x)) -> (forall F v, (forall t, vec_in t v -> p t) -> p (func F v)) -> forall (t : term), p t.
Proof.
intros f1 f2. eapply term_rect'.
- apply f1.
- intros. apply f2. intros t. induction 1; inversion X; subst; eauto.
apply Eqdep_dec.inj_pair2_eq_dec in H2; subst; eauto. decide equality.
Qed.
Lemma term_ind (p : term -> Prop) :
(forall x, p (var x)) -> (forall F v (IH : forall t, In t v -> p t), p (func F v)) -> forall (t : term), p t.
Proof.
intros f1 f2. eapply term_rect'.
- apply f1.
- intros. apply f2. intros t. induction 1 ; inversion X; subst; eauto.
apply Eqdep_dec.inj_pair2_eq_dec in H3; subst; eauto. decide equality.
Qed.
Inductive InTv {A : Type} (a : A) : forall n : nat, vec A n -> Type :=
InTv_cons_hd : forall (m : nat) (v : vec A m), InTv a (S m) (cons A a m v)
| InTv_cons_tl : forall (m : nat) (x : A) (v : vec A m), InTv a m v -> InTv a (S m) (cons A x m v).
Lemma term_indT (p : term -> Type) :
(forall x, p (var x)) -> (forall F v (IH : forall t, InTv t (ar_syms F) v -> p t), p (func F v)) -> forall (t : term), p t.
Proof.
intros f1 f2. eapply term_rect'.
- apply f1.
- intros. apply f2. intros t. induction 1 ; inversion X; subst; eauto.
apply Eqdep_dec.inj_pair2_eq_dec in H2; subst; eauto. decide equality.
Qed.
Lemma strong_term_ind' (p : term -> Type) :
(forall x, p (var x)) -> (forall F v, (Forall p v) -> p (func F v)) -> forall (t : term), p t.
Proof.
intros f1 f2. fix strong_term_ind' 1. destruct t as [n| F v].
- apply f1.
- apply f2. induction v.
+ econstructor.
+ econstructor. now eapply strong_term_ind'. eauto.
Qed.
Ltac resolve_existT := try
match goal with
| [ H2 : @existT ?X _ _ _ = existT _ _ _ |- _ ] => eapply Eqdep_dec.inj_pair2_eq_dec in H2; [subst | try (eauto || now intros; decide equality)]
end.
Ltac inv H :=
inversion H; subst; resolve_existT.
Lemma strong_term_ind (p : term -> Type) :
(forall x, p ($x)) -> (forall F v, (forall t, vec_in t v -> p t) -> p (func F v)) -> forall (t : term), p t.
Proof.
intros f1 f2. eapply strong_term_ind'.
- apply f1.
- intros. apply f2. intros t. induction 1 ; inv X ; eauto.
Qed.
(* Substitution induction principle for formulas *)
Fixpoint size (phi : form) :=
match phi with
| atom _ _ => 0
| bot => 0
| bin b phi psi => S (size phi + size psi)
| quant q phi => S (size phi)
end.
Lemma size_ind {X : Type} (f : X -> nat) (P : X -> Prop) :
(forall x, (forall y, f y < f x -> P y) -> P x) -> forall x, P x.
Proof.
intros H x. apply H.
induction (f x).
- intros y. lia.
- intros y. intro. assert (f y < n \/ f y = n) as [|] by lia.
+ apply IHn; lia.
+ apply H. rewrite H1. apply IHn.
Qed.
Lemma subst_size rho phi :
size (subst_form rho phi) = size phi.
Proof.
revert rho; induction phi; intros rho; cbn; congruence.
Qed.
Lemma form_ind_subst :
forall P : form -> Prop,
P bot ->
(forall P0 (t : vec term (ar_preds P0)), P (atom P0 t)) ->
(forall (b0 : binop) (f1 : form), P f1 -> forall f2 : form, P f2 -> P (bin b0 f1 f2)) ->
(forall (q : quantop) (f2 : form), (forall sigma, P (subst_form sigma f2)) -> P (quant q f2)) ->
forall (f4 : form), P f4.
Proof.
intros P H1 H3 H4 H5 phi. induction phi using (@size_ind _ size). destruct phi.
- apply H1.
- apply H3.
- apply H4; apply H; cbn; lia.
- apply H5. intros sigma. apply H. cbn. rewrite subst_size. lia.
Qed.
End fix_signature.
Ltac resolve_existT := try
match goal with
| [ H2 : @existT ?X _ _ _ = existT _ _ _ |- _ ] => eapply Eqdep_dec.inj_pair2_eq_dec in H2; [subst | try (eauto || now intros; decide equality)]
end.
Ltac inv H :=
inversion H; subst; resolve_existT.
(* ** Substitution lemmas *)
Section Subst.
Context {Σ_funcs : funcs_signature}.
Context {Σ_preds : preds_signature}.
Context {ops : operators}.
Lemma subst_term_ext (t : term) sigma tau :
(forall n, sigma n = tau n) -> t`[sigma] = t`[tau].
Proof.
intros H. induction t; cbn ; trivial.
- f_equal. now apply map_ext_in.
Qed.
Lemma subst_term_id (t : term) sigma :
(forall n, sigma n = var n) -> t`[sigma] = t.
Proof.
intros H. induction t; cbn ; trivial.
- f_equal. now erewrite map_ext_in, map_id.
Qed.
Lemma subst_term_var (t : term) :
t`[var] = t.
Proof.
now apply subst_term_id.
Qed.
Lemma subst_term_comp (t : term) sigma tau :
t`[sigma]`[tau] = t`[sigma >> subst_term tau].
Proof.
induction t; cbn ; trivial.
- f_equal. rewrite map_map. now apply map_ext_in.
Qed.
Lemma subst_term_shift (t : term) s :
t`[↑]`[s..] = t.
Proof.
rewrite subst_term_comp. apply subst_term_id. now intros [|].
Qed.
Lemma up_term (t : term) xi :
t`[↑]`[up xi] = t`[xi]`[↑].
Proof.
rewrite !subst_term_comp. apply subst_term_ext. reflexivity.
Qed.
Lemma up_ext sigma tau :
(forall n, sigma n = tau n) -> forall n, up sigma n = up tau n.
Proof.
destruct n; cbn; trivial.
unfold funcomp. now rewrite H.
Qed.
Lemma up_var sigma :
(forall n, sigma n = var n) -> forall n, up sigma n = var n.
Proof.
destruct n; cbn; trivial.
unfold funcomp. now rewrite H.
Qed.
Lemma up_funcomp sigma tau :
forall n, (up sigma >> subst_term (up tau)) n = up (sigma >> subst_term tau) n.
Proof.
intros [|]; cbn; trivial.
setoid_rewrite subst_term_comp.
apply subst_term_ext. now intros [|].
Qed.
Lemma subst_ext (phi : form) sigma tau :
(forall n, sigma n = tau n) -> phi[sigma] = phi[tau].
Proof.
induction phi in sigma, tau |- *; cbn; intros H.
- reflexivity.
- f_equal. apply map_ext. intros s. now apply subst_term_ext.
- now erewrite IHphi1, IHphi2.
- erewrite IHphi; trivial. now apply up_ext.
Qed.
Lemma subst_id (phi : form) sigma :
(forall n, sigma n = var n) -> phi[sigma] = phi.
Proof.
induction phi in sigma |- *; cbn; intros H.
- reflexivity.
- f_equal. erewrite map_ext; try apply map_id. intros s. now apply subst_term_id.
- now erewrite IHphi1, IHphi2.
- erewrite IHphi; trivial. now apply up_var.
Qed.
Lemma subst_var (phi : form) :
phi[var] = phi.
Proof.
now apply subst_id.
Qed.
Lemma subst_comp (phi : form) sigma tau :
phi[sigma][tau] = phi[sigma >> subst_term tau].
Proof.
induction phi in sigma, tau |- *; cbn.
- reflexivity.
- f_equal. rewrite map_map. apply map_ext. intros s. apply subst_term_comp.
- now rewrite IHphi1, IHphi2.
- rewrite IHphi. f_equal. now apply subst_ext, up_funcomp.
Qed.
Lemma subst_shift (phi : form) s :
phi[↑][s..] = phi.
Proof.
rewrite subst_comp. apply subst_id. now intros [|].
Qed.
Lemma up_form xi psi :
psi[↑][up xi] = psi[xi][↑].
Proof.
rewrite !subst_comp. apply subst_ext. reflexivity.
Qed.
Lemma up_decompose sigma phi :
phi[up (S >> sigma)][(sigma 0)..] = phi[sigma].
Proof.
rewrite subst_comp. apply subst_ext.
intros [].
- reflexivity.
- apply subst_term_shift.
Qed.
Lemma form_subst_help phi :
phi[up ↑][$0..] = phi.
Proof.
rewrite subst_comp. apply subst_id. now intros [].
Qed.
End Subst.
Section EqDec.
Context {Σ_funcs : funcs_signature}.
Context {Σ_preds : preds_signature}.
Context {eq_dec_preds : EqDec Σ_preds}.
Context {eq_dec_funcs : EqDec Σ_funcs}.
Lemma func_inv : forall f t0 t1, func f t0 = func f t1 -> t0 = t1.
Proof.
intros. inversion H; subst; try
match goal with
| [ H2 : @existT ?X _ _ _ = existT _ _ _ |- _ ] => eapply Eqdep_dec.inj_pair2_eq_dec in H2; [subst | try (eauto || now intros; decide equality)]
end. auto.
Qed.
Lemma atom_inv : forall P v0 v1, atom P v0 = atom P v1 -> v0 = v1.
Proof.
intros. inversion H; subst; try
match goal with
| [ H2 : @existT ?X _ _ _ = existT _ _ _ |- _ ] => eapply Eqdep_dec.inj_pair2_eq_dec in H2; [subst | try (eauto || now intros; decide equality)]
end. auto.
Qed.
Lemma eq_dec_nat : forall x y : nat, {x = y}+{x <> y}.
Proof.
induction x ; destruct y ; auto. destruct (IHx y) ; auto.
Qed.
Lemma vec_0_nil : forall (X : Type) (v : vec X 0),v = nil X.
Proof.
intro X.
pose (@VectorDef.case0 X (fun x => x = nil X)).
apply e. auto.
Qed.
Lemma eq_dec_preserved_vector : forall (X : Type) n (v0 : vec X n),
(forall t : X, InTv t n v0 -> forall y : X, {t = y} + {t <> y}) ->
(forall (v1 : vec X n), {v0 = v1}+{v0 <> v1}).
Proof.
intro X.
pose (t_rect X (fun (n : nat) (v0 : vec X n) =>
(forall t : X, InTv t n v0 -> forall y : X, {t = y} + {t <> y}) -> forall v1 : vec X n, {v0 = v1} + {v0 <> v1})).
apply s ; auto ; clear s.
- intros. left. pose (vec_0_nil X v1). auto.
- intros. pose (eta v1). rewrite e.
assert (J0: forall t0 : X, InTv t0 n t -> forall y : X, {t0 = y} + {t0 <> y}).
intros. apply X1. apply InTv_cons_tl. auto.
pose (X0 J0 (VectorDef.tl v1)). destruct s.
+ assert (J1: InTv h (S n) (cons X h n t)). apply InTv_cons_hd.
pose (X1 h J1). destruct (s (VectorDef.hd v1)).
* subst. auto.
* right. intro. apply cons_inj in H. destruct H. auto.
+ right. intro. apply cons_inj in H. destruct H. auto.
Qed.
Lemma eq_dec_preserved_vector0 : forall (X : Type),
(forall x y : X, {x = y} + {x <> y}) ->
(forall n (v0 v1 : vec X n), {v0 = v1}+{v0 <> v1}).
Proof.
intros X EDX n.
induction v0.
- intros. left. pose (vec_0_nil X v1). auto.
- intros. pose (eta v1). rewrite e. destruct (EDX h (VectorDef.hd v1)).
+ subst. destruct (IHv0 (VectorDef.tl v1)).
* left ; subst ; auto.
* right. intro. apply cons_inj in H. destruct H. subst. apply n0 ; auto.
+ right. intro. apply cons_inj in H. destruct H. subst. apply n0 ; auto.
Qed.
Lemma eq_dec_term : forall x y : term, {x = y}+{x <> y}.
Proof.
pose (term_indT (fun x => forall y : term, {x = y} + {x <> y})).
apply s ; clear s.
- intros. destruct y ; auto. destruct (eq_dec_nat x n) ; subst ; auto. right.
intro. inversion H ; auto. right ; congruence.
- intros. destruct y.
* right. intro. inversion H.
* pose (eq_dec_funcs F f). destruct s.
+ subst. pose (eq_dec_preserved_vector term (ar_syms f) v IH).
destruct (s t).
-- subst. auto.
-- right. intro. apply func_inv in H. auto.
+ right. intro. inversion H. subst. auto.
Qed.
Lemma eq_dec_form : forall x y : form, {x = y}+{x <> y}.
Proof.
induction x ; destruct y ; auto.
1-4: right ; intro ; inversion H.
2-5: right ; intro ; inversion H.
3-6: right ; intro ; inversion H.
- destruct (eq_dec_preds P P0) ; subst.
2: right ; intro ; inversion H ; auto.
assert (J1: (forall t0 : term, InTv t0 (ar_preds P0) t -> forall y : term, {t0 = y} + {t0 <> y})).
intros. apply eq_dec_term.
pose (eq_dec_preserved_vector term (ar_preds P0) t J1). destruct (s t0) ; subst ; auto.
right. intro. apply n. apply atom_inv in H. auto.
- destruct b ; destruct b0 ; auto.
2-4: right ; intro ; inversion H.
3-5: right ; intro ; inversion H.
1-3: destruct (IHx1 y1) ; destruct (IHx2 y2) ; subst ; auto ; right ; intro ; inversion H ; auto.
- destruct q ; destruct q0 ; subst. 2-3: right ; intro ; inversion H.
1-2: destruct (IHx y) ; subst ; auto ; right ; intro ; inversion H ; auto.
Qed.
Lemma form_all phi :
{ psi | phi = ∀ psi } + (~ exists psi, phi = ∀ psi).
Proof.
destruct phi; try destruct q. 1-3,5: right; intros [psi H]; discriminate.
left. exists phi. reflexivity.
Qed.
Lemma form_ex phi :
{ psi | phi = ∃ psi } + (~ exists psi, phi = ∃ psi).
Proof.
destruct phi; try destruct q. 1-4: right; intros [psi H]; discriminate.
left. exists phi. reflexivity.
Qed.
End EqDec.
Section PredicateSubstitution.
(* Atom substitution. *)
Context {Σ_funcs : funcs_signature}.
Context {Σ_preds : preds_signature}.
Context {ops : operators}.
Fixpoint atom_subst (s : forall (P : Σ_preds), Vector.t (@term Σ_funcs) (ar_preds P) -> form) (phi : form) :=
match phi with
| bot => bot
| atom P t => s P t
| bin b phi psi => bin b (atom_subst s phi) (atom_subst s psi)
| quant q phi => quant q (atom_subst s phi)
end.
Notation "phi [ s '/atom' ]" := (atom_subst s phi) (at level 7, left associativity) : subst_scope.
Definition atom_subst_respects (s : forall (P : Σ_preds), Vector.t (@term Σ_funcs) (ar_preds P) -> form)
:= forall P v sigma, (s P v)[sigma>> var] = s P (map (subst_term (sigma >> var)) v).
Definition atom_subst_respects_strong (s : forall (P : Σ_preds), Vector.t (@term Σ_funcs) (ar_preds P) -> form)
:= forall P v sigma, (s P v)[sigma] = s P (map (subst_term (sigma)) v).
Lemma atom_subst_strong_to_normal s : atom_subst_respects_strong s -> atom_subst_respects s.
Proof.
intros. intro. intros. auto.
Qed.
Lemma atom_subst_id phi : phi[ atom /atom] = phi.
Proof.
induction phi.
- easy.
- cbn. easy.
- cbn. rewrite IHphi1. now rewrite IHphi2.
- cbn. now rewrite IHphi.
Qed.
Lemma up_var_comp rho x : (up (rho >> var)) x = ((fun n => match n with 0 => 0 | S n => S (rho n) end) >>var) x.
Proof.
now destruct x.
Qed.
Lemma atom_subst_comp s rho phi : atom_subst_respects s -> phi[s/atom][rho>>var] = phi[rho>>var][s/atom].
Proof.
intros Hresp.
induction phi in s,rho,Hresp|-*.
- easy.
- cbn. easy.
- cbn. rewrite IHphi1. 1: now rewrite IHphi2. easy.
- cbn. f_equal. rewrite ! (subst_ext _ _ _ (up_var_comp _) ). rewrite IHphi. 1:easy.
easy.
Qed.
Lemma atom_subst_comp_strong s rho phi :
atom_subst_respects_strong s -> phi[s/atom][rho] = phi[rho][s/atom].
Proof.
intros Hresp.
induction phi in s,rho,Hresp|-*.
- easy.
- cbn. easy.
- cbn. rewrite IHphi1. 1: now rewrite IHphi2. easy.
- cbn. now rewrite IHphi.
Qed.
End PredicateSubstitution.
#[global] Notation "phi [ s '/atom' ]" := (atom_subst s phi) (at level 7, left associativity) : subst_scope.
Require Import Ensembles.
Require Import Coq.Vectors.Vector.
Local Notation vec := t.
From Equations Require Export Equations.
(* Some preliminary definitions for substitions *)
Definition scons {X: Type} (x : X) (xi : nat -> X) :=
fun n => match n with
| 0 => x
| S n => xi n
end.
Definition funcomp {X Y Z} (g : Y -> Z) (f : X -> Y) :=
fun x => g (f x).
(* Signatures are a record to allow for easier definitions of general transformations on signatures *)
Class funcs_signature :=
{ syms : Type; ar_syms : syms -> nat }.
Coercion syms : funcs_signature >-> Sortclass.
Class preds_signature :=
{ preds : Type; ar_preds : preds -> nat }.
Coercion preds : preds_signature >-> Sortclass.
Section fix_signature.
Context {Σ_funcs : funcs_signature}.
(* We use the stdlib definition of vectors to be maximally compatible *)
Unset Elimination Schemes.
Inductive term : Type :=
| var : nat -> term
| func : forall (f : syms), vec term (ar_syms f) -> term.
Set Elimination Schemes.
Fixpoint subst_term (σ : nat -> term) (t : term) : term :=
match t with
| var n => σ n
| func f v => func f (map (subst_term σ) v)
end.
Context {Σ_preds : preds_signature}.
(* Syntax is parametrised in binary operators and quantifiers.
Most developments will fix these types in the beginning and never change them.
*)
Class operators := {binop : Type ; quantop : Type}.
Context {ops : operators}.
Inductive form : Type :=
| bot : form
| atom : forall (P : preds), vec term (ar_preds P) -> form
| bin : binop -> form -> form -> form
| quant : quantop -> form -> form.
Definition up (σ : nat -> term) := scons (var 0) (funcomp (subst_term (funcomp var S)) σ).
Fixpoint subst_form (σ : nat -> term) (phi : form) : form :=
match phi with
| bot => bot
| atom P v => atom P (map (subst_term σ) v)
| bin op phi1 phi2 => bin op (subst_form σ phi1) (subst_form σ phi2)
| quant op phi => quant op (subst_form (up σ) phi)
end.
End fix_signature.
(* Setting implicit arguments is crucial *)
(* We can write term both with and without arguments, but printing is without. *)
Arguments term _, {_}.
Arguments var _ _, {_} _.
Arguments func _ _ _, {_} _ _.
Arguments subst_term {_} _ _.
(* Formulas can be written with the signatures explicit or not.
If the operations are explicit, the signatures are too.
*)
Arguments form _ _ _ , _ _ {_}, {_ _ _}.
Arguments atom _ _ _ , _ _ {_}, {_ _ _}.
Arguments bin _ _ _ , _ _ {_}, {_ _ _}.
Arguments quant _ _ _ , _ _ {_}, {_ _ _}.
Arguments up _, {_}.
Arguments subst_form _ _ _, _ _ {_}, {_ _ _}.
(* Substitution Notation *)
Declare Scope subst_scope.
Open Scope subst_scope.
Notation "$ x" := (var x) (at level 3, format "$ '/' x") : subst_scope.
Notation "t `[ sigma ]" := (subst_term sigma t) (at level 7, left associativity, format "t '/' `[ sigma ]") : subst_scope.
Notation "phi [ sigma ]" := (subst_form sigma phi) (at level 7, left associativity, format "phi '/' [ sigma ]") : subst_scope.
Notation "s .: sigma" := (scons s sigma) (at level 70, right associativity) : subst_scope.
Notation "f >> g" := (funcomp g f) (at level 50) : subst_scope.
Notation "s '..'" := (scons s var) (at level 4, format "s ..") : subst_scope.
Notation "↑" := (S >> var) : subst_scope.
(* Full syntax *)
Declare Scope syn.
Open Scope syn.
Module FullSyntax.
Inductive full_logic_sym : Type :=
| Conj : full_logic_sym
| Disj : full_logic_sym
| Impl : full_logic_sym.
Inductive full_logic_quant : Type :=
| All : full_logic_quant
| Ex : full_logic_quant.
Definition full_operators : operators :=
{| binop := full_logic_sym ; quantop := full_logic_quant |}.
#[export] Hint Immediate full_operators : typeclass_instances.
Notation "∀ Phi" := (@quant _ _ full_operators All Phi) (at level 50) : syn.
Notation "∃ Phi" := (@quant _ _ full_operators Ex Phi) (at level 50) : syn.
Notation "A ∧ B" := (@bin _ _ full_operators Conj A B) (at level 41) : syn.
Notation "A ∨ B" := (@bin _ _ full_operators Disj A B) (at level 42) : syn.
Notation "A '-->' B" := (@bin _ _ full_operators Impl A B) (at level 43, right associativity) : syn.
Notation "⊥" := (bot) : syn.
Notation "⊤" := (⊥ --> ⊥) : syn.
Notation "¬ A" := (A --> ⊥) (at level 42) : syn.
Notation "A '<-->' B" := ((A --> B) ∧ (B --> A)) (at level 43) : syn.
End FullSyntax.
Export FullSyntax.
Section fix_signature.
Context {Σ_funcs : funcs_signature}.
Context {Σ_preds : preds_signature}.
(* Example formula: *)
Compute (∀ ⊥ --> ⊥).
Context {ops : operators}.
(* Induction principle for terms *)
Inductive Forall {A : Type} (P : A -> Type) : forall {n}, t A n -> Type :=
| Forall_nil : Forall P (@Vector.nil A)
| Forall_cons : forall n (x : A) (l : t A n), P x -> Forall P l -> Forall P (@Vector.cons A x n l).
Inductive vec_in {A : Type} (a : A) : forall {n}, t A n -> Type :=
| vec_inB {n} (v : t A n) : vec_in a (cons A a n v)
| vec_inS a' {n} (v : t A n) : vec_in a v -> vec_in a (cons A a' n v).
Hint Constructors vec_in : core.
Lemma term_rect' (p : term -> Type) :
(forall x, p (var x)) -> (forall F v, (Forall p v) -> p (func F v)) -> forall (t : term), p t.
Proof.
intros f1 f2. fix strong_term_ind' 1. destruct t as [n | F v].
- apply f1.
- apply f2. induction v.
+ econstructor.
+ econstructor. now eapply strong_term_ind'. eauto.
Qed.
Lemma term_rect (p : term -> Type) :
(forall x, p (var x)) -> (forall F v, (forall t, vec_in t v -> p t) -> p (func F v)) -> forall (t : term), p t.
Proof.
intros f1 f2. eapply term_rect'.
- apply f1.
- intros. apply f2. intros t. induction 1; inversion X; subst; eauto.
apply Eqdep_dec.inj_pair2_eq_dec in H2; subst; eauto. decide equality.
Qed.
Lemma term_ind (p : term -> Prop) :
(forall x, p (var x)) -> (forall F v (IH : forall t, In t v -> p t), p (func F v)) -> forall (t : term), p t.
Proof.
intros f1 f2. eapply term_rect'.
- apply f1.
- intros. apply f2. intros t. induction 1 ; inversion X; subst; eauto.
apply Eqdep_dec.inj_pair2_eq_dec in H3; subst; eauto. decide equality.
Qed.
Inductive InTv {A : Type} (a : A) : forall n : nat, vec A n -> Type :=
InTv_cons_hd : forall (m : nat) (v : vec A m), InTv a (S m) (cons A a m v)
| InTv_cons_tl : forall (m : nat) (x : A) (v : vec A m), InTv a m v -> InTv a (S m) (cons A x m v).
Lemma term_indT (p : term -> Type) :
(forall x, p (var x)) -> (forall F v (IH : forall t, InTv t (ar_syms F) v -> p t), p (func F v)) -> forall (t : term), p t.
Proof.
intros f1 f2. eapply term_rect'.
- apply f1.
- intros. apply f2. intros t. induction 1 ; inversion X; subst; eauto.
apply Eqdep_dec.inj_pair2_eq_dec in H2; subst; eauto. decide equality.
Qed.
Lemma strong_term_ind' (p : term -> Type) :
(forall x, p (var x)) -> (forall F v, (Forall p v) -> p (func F v)) -> forall (t : term), p t.
Proof.
intros f1 f2. fix strong_term_ind' 1. destruct t as [n| F v].
- apply f1.
- apply f2. induction v.
+ econstructor.
+ econstructor. now eapply strong_term_ind'. eauto.
Qed.
Ltac resolve_existT := try
match goal with
| [ H2 : @existT ?X _ _ _ = existT _ _ _ |- _ ] => eapply Eqdep_dec.inj_pair2_eq_dec in H2; [subst | try (eauto || now intros; decide equality)]
end.
Ltac inv H :=
inversion H; subst; resolve_existT.
Lemma strong_term_ind (p : term -> Type) :
(forall x, p ($x)) -> (forall F v, (forall t, vec_in t v -> p t) -> p (func F v)) -> forall (t : term), p t.
Proof.
intros f1 f2. eapply strong_term_ind'.
- apply f1.
- intros. apply f2. intros t. induction 1 ; inv X ; eauto.
Qed.
(* Substitution induction principle for formulas *)
Fixpoint size (phi : form) :=
match phi with
| atom _ _ => 0
| bot => 0
| bin b phi psi => S (size phi + size psi)
| quant q phi => S (size phi)
end.
Lemma size_ind {X : Type} (f : X -> nat) (P : X -> Prop) :
(forall x, (forall y, f y < f x -> P y) -> P x) -> forall x, P x.
Proof.
intros H x. apply H.
induction (f x).
- intros y. lia.
- intros y. intro. assert (f y < n \/ f y = n) as [|] by lia.
+ apply IHn; lia.
+ apply H. rewrite H1. apply IHn.
Qed.
Lemma subst_size rho phi :
size (subst_form rho phi) = size phi.
Proof.
revert rho; induction phi; intros rho; cbn; congruence.
Qed.
Lemma form_ind_subst :
forall P : form -> Prop,
P bot ->
(forall P0 (t : vec term (ar_preds P0)), P (atom P0 t)) ->
(forall (b0 : binop) (f1 : form), P f1 -> forall f2 : form, P f2 -> P (bin b0 f1 f2)) ->
(forall (q : quantop) (f2 : form), (forall sigma, P (subst_form sigma f2)) -> P (quant q f2)) ->
forall (f4 : form), P f4.
Proof.
intros P H1 H3 H4 H5 phi. induction phi using (@size_ind _ size). destruct phi.
- apply H1.
- apply H3.
- apply H4; apply H; cbn; lia.
- apply H5. intros sigma. apply H. cbn. rewrite subst_size. lia.
Qed.
End fix_signature.
Ltac resolve_existT := try
match goal with
| [ H2 : @existT ?X _ _ _ = existT _ _ _ |- _ ] => eapply Eqdep_dec.inj_pair2_eq_dec in H2; [subst | try (eauto || now intros; decide equality)]
end.
Ltac inv H :=
inversion H; subst; resolve_existT.
(* ** Substitution lemmas *)
Section Subst.
Context {Σ_funcs : funcs_signature}.
Context {Σ_preds : preds_signature}.
Context {ops : operators}.
Lemma subst_term_ext (t : term) sigma tau :
(forall n, sigma n = tau n) -> t`[sigma] = t`[tau].
Proof.
intros H. induction t; cbn ; trivial.
- f_equal. now apply map_ext_in.
Qed.
Lemma subst_term_id (t : term) sigma :
(forall n, sigma n = var n) -> t`[sigma] = t.
Proof.
intros H. induction t; cbn ; trivial.
- f_equal. now erewrite map_ext_in, map_id.
Qed.
Lemma subst_term_var (t : term) :
t`[var] = t.
Proof.
now apply subst_term_id.
Qed.
Lemma subst_term_comp (t : term) sigma tau :
t`[sigma]`[tau] = t`[sigma >> subst_term tau].
Proof.
induction t; cbn ; trivial.
- f_equal. rewrite map_map. now apply map_ext_in.
Qed.
Lemma subst_term_shift (t : term) s :
t`[↑]`[s..] = t.
Proof.
rewrite subst_term_comp. apply subst_term_id. now intros [|].
Qed.
Lemma up_term (t : term) xi :
t`[↑]`[up xi] = t`[xi]`[↑].
Proof.
rewrite !subst_term_comp. apply subst_term_ext. reflexivity.
Qed.
Lemma up_ext sigma tau :
(forall n, sigma n = tau n) -> forall n, up sigma n = up tau n.
Proof.
destruct n; cbn; trivial.
unfold funcomp. now rewrite H.
Qed.
Lemma up_var sigma :
(forall n, sigma n = var n) -> forall n, up sigma n = var n.
Proof.
destruct n; cbn; trivial.
unfold funcomp. now rewrite H.
Qed.
Lemma up_funcomp sigma tau :
forall n, (up sigma >> subst_term (up tau)) n = up (sigma >> subst_term tau) n.
Proof.
intros [|]; cbn; trivial.
setoid_rewrite subst_term_comp.
apply subst_term_ext. now intros [|].
Qed.
Lemma subst_ext (phi : form) sigma tau :
(forall n, sigma n = tau n) -> phi[sigma] = phi[tau].
Proof.
induction phi in sigma, tau |- *; cbn; intros H.
- reflexivity.
- f_equal. apply map_ext. intros s. now apply subst_term_ext.
- now erewrite IHphi1, IHphi2.
- erewrite IHphi; trivial. now apply up_ext.
Qed.
Lemma subst_id (phi : form) sigma :
(forall n, sigma n = var n) -> phi[sigma] = phi.
Proof.
induction phi in sigma |- *; cbn; intros H.
- reflexivity.
- f_equal. erewrite map_ext; try apply map_id. intros s. now apply subst_term_id.
- now erewrite IHphi1, IHphi2.
- erewrite IHphi; trivial. now apply up_var.
Qed.
Lemma subst_var (phi : form) :
phi[var] = phi.
Proof.
now apply subst_id.
Qed.
Lemma subst_comp (phi : form) sigma tau :
phi[sigma][tau] = phi[sigma >> subst_term tau].
Proof.
induction phi in sigma, tau |- *; cbn.
- reflexivity.
- f_equal. rewrite map_map. apply map_ext. intros s. apply subst_term_comp.
- now rewrite IHphi1, IHphi2.
- rewrite IHphi. f_equal. now apply subst_ext, up_funcomp.
Qed.
Lemma subst_shift (phi : form) s :
phi[↑][s..] = phi.
Proof.
rewrite subst_comp. apply subst_id. now intros [|].
Qed.
Lemma up_form xi psi :
psi[↑][up xi] = psi[xi][↑].
Proof.
rewrite !subst_comp. apply subst_ext. reflexivity.
Qed.
Lemma up_decompose sigma phi :
phi[up (S >> sigma)][(sigma 0)..] = phi[sigma].
Proof.
rewrite subst_comp. apply subst_ext.
intros [].
- reflexivity.
- apply subst_term_shift.
Qed.
Lemma form_subst_help phi :
phi[up ↑][$0..] = phi.
Proof.
rewrite subst_comp. apply subst_id. now intros [].
Qed.
End Subst.
Section EqDec.
Context {Σ_funcs : funcs_signature}.
Context {Σ_preds : preds_signature}.
Context {eq_dec_preds : EqDec Σ_preds}.
Context {eq_dec_funcs : EqDec Σ_funcs}.
Lemma func_inv : forall f t0 t1, func f t0 = func f t1 -> t0 = t1.
Proof.
intros. inversion H; subst; try
match goal with
| [ H2 : @existT ?X _ _ _ = existT _ _ _ |- _ ] => eapply Eqdep_dec.inj_pair2_eq_dec in H2; [subst | try (eauto || now intros; decide equality)]
end. auto.
Qed.
Lemma atom_inv : forall P v0 v1, atom P v0 = atom P v1 -> v0 = v1.
Proof.
intros. inversion H; subst; try
match goal with
| [ H2 : @existT ?X _ _ _ = existT _ _ _ |- _ ] => eapply Eqdep_dec.inj_pair2_eq_dec in H2; [subst | try (eauto || now intros; decide equality)]
end. auto.
Qed.
Lemma eq_dec_nat : forall x y : nat, {x = y}+{x <> y}.
Proof.
induction x ; destruct y ; auto. destruct (IHx y) ; auto.
Qed.
Lemma vec_0_nil : forall (X : Type) (v : vec X 0),v = nil X.
Proof.
intro X.
pose (@VectorDef.case0 X (fun x => x = nil X)).
apply e. auto.
Qed.
Lemma eq_dec_preserved_vector : forall (X : Type) n (v0 : vec X n),
(forall t : X, InTv t n v0 -> forall y : X, {t = y} + {t <> y}) ->
(forall (v1 : vec X n), {v0 = v1}+{v0 <> v1}).
Proof.
intro X.
pose (t_rect X (fun (n : nat) (v0 : vec X n) =>
(forall t : X, InTv t n v0 -> forall y : X, {t = y} + {t <> y}) -> forall v1 : vec X n, {v0 = v1} + {v0 <> v1})).
apply s ; auto ; clear s.
- intros. left. pose (vec_0_nil X v1). auto.
- intros. pose (eta v1). rewrite e.
assert (J0: forall t0 : X, InTv t0 n t -> forall y : X, {t0 = y} + {t0 <> y}).
intros. apply X1. apply InTv_cons_tl. auto.
pose (X0 J0 (VectorDef.tl v1)). destruct s.
+ assert (J1: InTv h (S n) (cons X h n t)). apply InTv_cons_hd.
pose (X1 h J1). destruct (s (VectorDef.hd v1)).
* subst. auto.
* right. intro. apply cons_inj in H. destruct H. auto.
+ right. intro. apply cons_inj in H. destruct H. auto.
Qed.
Lemma eq_dec_preserved_vector0 : forall (X : Type),
(forall x y : X, {x = y} + {x <> y}) ->
(forall n (v0 v1 : vec X n), {v0 = v1}+{v0 <> v1}).
Proof.
intros X EDX n.
induction v0.
- intros. left. pose (vec_0_nil X v1). auto.
- intros. pose (eta v1). rewrite e. destruct (EDX h (VectorDef.hd v1)).
+ subst. destruct (IHv0 (VectorDef.tl v1)).
* left ; subst ; auto.
* right. intro. apply cons_inj in H. destruct H. subst. apply n0 ; auto.
+ right. intro. apply cons_inj in H. destruct H. subst. apply n0 ; auto.
Qed.
Lemma eq_dec_term : forall x y : term, {x = y}+{x <> y}.
Proof.
pose (term_indT (fun x => forall y : term, {x = y} + {x <> y})).
apply s ; clear s.
- intros. destruct y ; auto. destruct (eq_dec_nat x n) ; subst ; auto. right.
intro. inversion H ; auto. right ; congruence.
- intros. destruct y.
* right. intro. inversion H.
* pose (eq_dec_funcs F f). destruct s.
+ subst. pose (eq_dec_preserved_vector term (ar_syms f) v IH).
destruct (s t).
-- subst. auto.
-- right. intro. apply func_inv in H. auto.
+ right. intro. inversion H. subst. auto.
Qed.
Lemma eq_dec_form : forall x y : form, {x = y}+{x <> y}.
Proof.
induction x ; destruct y ; auto.
1-4: right ; intro ; inversion H.
2-5: right ; intro ; inversion H.
3-6: right ; intro ; inversion H.
- destruct (eq_dec_preds P P0) ; subst.
2: right ; intro ; inversion H ; auto.
assert (J1: (forall t0 : term, InTv t0 (ar_preds P0) t -> forall y : term, {t0 = y} + {t0 <> y})).
intros. apply eq_dec_term.
pose (eq_dec_preserved_vector term (ar_preds P0) t J1). destruct (s t0) ; subst ; auto.
right. intro. apply n. apply atom_inv in H. auto.
- destruct b ; destruct b0 ; auto.
2-4: right ; intro ; inversion H.
3-5: right ; intro ; inversion H.
1-3: destruct (IHx1 y1) ; destruct (IHx2 y2) ; subst ; auto ; right ; intro ; inversion H ; auto.
- destruct q ; destruct q0 ; subst. 2-3: right ; intro ; inversion H.
1-2: destruct (IHx y) ; subst ; auto ; right ; intro ; inversion H ; auto.
Qed.
Lemma form_all phi :
{ psi | phi = ∀ psi } + (~ exists psi, phi = ∀ psi).
Proof.
destruct phi; try destruct q. 1-3,5: right; intros [psi H]; discriminate.
left. exists phi. reflexivity.
Qed.
Lemma form_ex phi :
{ psi | phi = ∃ psi } + (~ exists psi, phi = ∃ psi).
Proof.
destruct phi; try destruct q. 1-4: right; intros [psi H]; discriminate.
left. exists phi. reflexivity.
Qed.
End EqDec.
Section PredicateSubstitution.
(* Atom substitution. *)
Context {Σ_funcs : funcs_signature}.
Context {Σ_preds : preds_signature}.
Context {ops : operators}.
Fixpoint atom_subst (s : forall (P : Σ_preds), Vector.t (@term Σ_funcs) (ar_preds P) -> form) (phi : form) :=
match phi with
| bot => bot
| atom P t => s P t
| bin b phi psi => bin b (atom_subst s phi) (atom_subst s psi)
| quant q phi => quant q (atom_subst s phi)
end.
Notation "phi [ s '/atom' ]" := (atom_subst s phi) (at level 7, left associativity) : subst_scope.
Definition atom_subst_respects (s : forall (P : Σ_preds), Vector.t (@term Σ_funcs) (ar_preds P) -> form)
:= forall P v sigma, (s P v)[sigma>> var] = s P (map (subst_term (sigma >> var)) v).
Definition atom_subst_respects_strong (s : forall (P : Σ_preds), Vector.t (@term Σ_funcs) (ar_preds P) -> form)
:= forall P v sigma, (s P v)[sigma] = s P (map (subst_term (sigma)) v).
Lemma atom_subst_strong_to_normal s : atom_subst_respects_strong s -> atom_subst_respects s.
Proof.
intros. intro. intros. auto.
Qed.
Lemma atom_subst_id phi : phi[ atom /atom] = phi.
Proof.
induction phi.
- easy.
- cbn. easy.
- cbn. rewrite IHphi1. now rewrite IHphi2.
- cbn. now rewrite IHphi.
Qed.
Lemma up_var_comp rho x : (up (rho >> var)) x = ((fun n => match n with 0 => 0 | S n => S (rho n) end) >>var) x.
Proof.
now destruct x.
Qed.
Lemma atom_subst_comp s rho phi : atom_subst_respects s -> phi[s/atom][rho>>var] = phi[rho>>var][s/atom].
Proof.
intros Hresp.
induction phi in s,rho,Hresp|-*.
- easy.
- cbn. easy.
- cbn. rewrite IHphi1. 1: now rewrite IHphi2. easy.
- cbn. f_equal. rewrite ! (subst_ext _ _ _ (up_var_comp _) ). rewrite IHphi. 1:easy.
easy.
Qed.
Lemma atom_subst_comp_strong s rho phi :
atom_subst_respects_strong s -> phi[s/atom][rho] = phi[rho][s/atom].
Proof.
intros Hresp.
induction phi in s,rho,Hresp|-*.
- easy.
- cbn. easy.
- cbn. rewrite IHphi1. 1: now rewrite IHphi2. easy.
- cbn. now rewrite IHphi.
Qed.
End PredicateSubstitution.
#[global] Notation "phi [ s '/atom' ]" := (atom_subst s phi) (at level 7, left associativity) : subst_scope.