From PostTheorem Require Import Shared.Libs.PSL.Vectors.Vectors Shared.Libs.PSL.Vectors.VectorForall.
Require Import List.
Import ListNotations.
Import Coq.Vectors.Vector.
Local Notation vec := t.
Set Default Proof Using "Type".
Inductive peirce := class | intu.
Existing Class peirce.
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).
Fixpoint iter {X: Type} f n (x : X) :=
match n with
0 => x
| S m => f (iter f m x)
end.
Fact iter_switch {X} f n x :
f (@iter X f n x) = iter f n (f x).
Proof.
induction n; cbn; now try rewrite IHn.
Qed.
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}.
Unset Elimination Schemes.
Inductive term : Type :=
| var : nat -> term
| func : forall (f : syms), vec term (ar_syms f) -> term.
Arguments func _ _ : clear implicits.
Lemma term_rect' (p : term -> Type) :
(forall x, p (var x)) -> (forall F v, (ForallT 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, Vector_In2 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.
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.
Qed.
Set Elimination Schemes.
Fixpoint subst_term (σ : nat -> term) (t : term) : term :=
match t with
| var t => σ t
| func f v => func f (map (subst_term σ) v)
end.
Context {Σ_preds : preds_signature}.
Inductive falsity_flag := falsity_off | falsity_on.
Existing Class falsity_flag.
Existing Instance falsity_on | 1.
Existing Instance falsity_off | 0.
Class operators := {binop : Type ; quantop : Type}.
Context {ops : operators}.
Inductive form : falsity_flag -> Type :=
| falsity : form falsity_on
| atom {b} : forall (P : preds), vec term (ar_preds P) -> form b
| bin {b} : binop -> form b -> form b -> form b
| quant {b} : quantop -> form b -> form b.
Arguments form {_}.
Arguments atom {_} _ _, _ _ _.
Arguments bin {_} _ _ _, _ _ _ _.
Arguments quant {_} _ _, _ _ _.
Definition up (σ : nat -> term) := scons (var 0) (funcomp (subst_term (funcomp var S)) σ).
Fixpoint subst_form `{falsity_flag} (σ : nat -> term) (phi : form) : form :=
match phi with
| falsity => falsity
| 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.
Arguments term _, {_}.
Arguments var _ _, {_} _.
Arguments func _ _ _, {_} _ _.
Arguments subst_term {_} _ _.
Arguments form _ _ _ _, _ _ {_ _}, {_ _ _ _}, {_ _ _} _.
Arguments atom _ _ _ _, _ _ {_ _}, {_ _ _ _}.
Arguments bin _ _ _ _, _ _ {_ _}, {_ _ _ _}.
Arguments quant _ _ _ _, _ _ {_ _}, {_ _ _ _}.
Arguments up _, {_}.
Arguments subst_form _ _ _ _, _ _ {_ _}, {_ _ _ _}.
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.
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.
Declare Scope full_syntax.
Delimit Scope full_syntax with Ffull.
#[global] Open Scope full_syntax.
Notation "∀ Phi" := (@quant _ _ full_operators _ All Phi) (at level 50) : full_syntax.
Notation "∃ Phi" := (@quant _ _ full_operators _ Ex Phi) (at level 50) : full_syntax.
Notation "A ∧ B" := (@bin _ _ full_operators _ Conj A B) (at level 41) : full_syntax.
Notation "A ∨ B" := (@bin _ _ full_operators _ Disj A B) (at level 42) : full_syntax.
Notation "A → B" := (@bin _ _ full_operators _ Impl A B) (at level 43, right associativity) : full_syntax.
Notation "⊥" := (falsity) : full_syntax.
Notation "¬ A" := (A → ⊥) (at level 42) : full_syntax.
Notation "A ↔ B" := ((A → B) ∧ (B → A)) (at level 43) : full_syntax.
Fixpoint impl {Σ_funcs : funcs_signature} {Σ_preds : preds_signature} {ff : falsity_flag} (A : list form) phi :=
match A with
| [] => phi
| psi :: A => bin _ _ full_operators _ Impl psi (impl A phi)
end.
Notation "A ==> phi" := (impl A phi) (right associativity, at level 55).
Definition exist_times {Σ_funcs : funcs_signature} {Σ_preds : preds_signature} {ff : falsity_flag} n (phi : form) := iter (fun psi => ∃ psi) n phi.
Definition forall_times {Σ_funcs : funcs_signature} {Σ_preds : preds_signature} {ff : falsity_flag} n (phi : form) := iter (fun psi => ∀ psi) n phi.
End FullSyntax.
Module FragmentSyntax.
Inductive frag_logic_binop : Type :=
| Impl : frag_logic_binop.
Inductive frag_logic_quant : Type :=
| All : frag_logic_quant.
Definition frag_operators : operators :=
{| binop := frag_logic_binop ; quantop := frag_logic_quant |}.
#[export] Hint Immediate frag_operators : typeclass_instances.
Declare Scope fragment_syntax.
Delimit Scope fragment_syntax with Ffrag.
#[global] Open Scope fragment_syntax.
Notation "∀ Phi" := (@quant _ _ frag_operators _ All Phi) (at level 50) : fragment_syntax.
Notation "phi → psi" := (@bin _ _ frag_operators _ Impl phi psi) (at level 43, right associativity) : fragment_syntax.
Notation "¬ phi" := (phi → falsity) (at level 42) : fragment_syntax.
Notation "⊥" := (falsity) : fragment_syntax.
Fixpoint impl {Σ_funcs : funcs_signature} {Σ_preds : preds_signature} {ff : falsity_flag} (A : list form) phi :=
match A with
| [] => phi
| psi :: A => bin _ _ frag_operators _ Impl psi (impl A phi)
end.
Notation "A ==> phi" := (impl A phi) (right associativity, at level 55).
Definition forall_times {Σ_funcs : funcs_signature} {Σ_preds : preds_signature} {ff : falsity_flag} n (phi : form) := iter (fun psi => ∀ psi) n phi.
End FragmentSyntax.
Require Import List.
Import ListNotations.
Import Coq.Vectors.Vector.
Local Notation vec := t.
Set Default Proof Using "Type".
Inductive peirce := class | intu.
Existing Class peirce.
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).
Fixpoint iter {X: Type} f n (x : X) :=
match n with
0 => x
| S m => f (iter f m x)
end.
Fact iter_switch {X} f n x :
f (@iter X f n x) = iter f n (f x).
Proof.
induction n; cbn; now try rewrite IHn.
Qed.
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}.
Unset Elimination Schemes.
Inductive term : Type :=
| var : nat -> term
| func : forall (f : syms), vec term (ar_syms f) -> term.
Arguments func _ _ : clear implicits.
Lemma term_rect' (p : term -> Type) :
(forall x, p (var x)) -> (forall F v, (ForallT 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, Vector_In2 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.
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.
Qed.
Set Elimination Schemes.
Fixpoint subst_term (σ : nat -> term) (t : term) : term :=
match t with
| var t => σ t
| func f v => func f (map (subst_term σ) v)
end.
Context {Σ_preds : preds_signature}.
Inductive falsity_flag := falsity_off | falsity_on.
Existing Class falsity_flag.
Existing Instance falsity_on | 1.
Existing Instance falsity_off | 0.
Class operators := {binop : Type ; quantop : Type}.
Context {ops : operators}.
Inductive form : falsity_flag -> Type :=
| falsity : form falsity_on
| atom {b} : forall (P : preds), vec term (ar_preds P) -> form b
| bin {b} : binop -> form b -> form b -> form b
| quant {b} : quantop -> form b -> form b.
Arguments form {_}.
Arguments atom {_} _ _, _ _ _.
Arguments bin {_} _ _ _, _ _ _ _.
Arguments quant {_} _ _, _ _ _.
Definition up (σ : nat -> term) := scons (var 0) (funcomp (subst_term (funcomp var S)) σ).
Fixpoint subst_form `{falsity_flag} (σ : nat -> term) (phi : form) : form :=
match phi with
| falsity => falsity
| 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.
Arguments term _, {_}.
Arguments var _ _, {_} _.
Arguments func _ _ _, {_} _ _.
Arguments subst_term {_} _ _.
Arguments form _ _ _ _, _ _ {_ _}, {_ _ _ _}, {_ _ _} _.
Arguments atom _ _ _ _, _ _ {_ _}, {_ _ _ _}.
Arguments bin _ _ _ _, _ _ {_ _}, {_ _ _ _}.
Arguments quant _ _ _ _, _ _ {_ _}, {_ _ _ _}.
Arguments up _, {_}.
Arguments subst_form _ _ _ _, _ _ {_ _}, {_ _ _ _}.
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.
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.
Declare Scope full_syntax.
Delimit Scope full_syntax with Ffull.
#[global] Open Scope full_syntax.
Notation "∀ Phi" := (@quant _ _ full_operators _ All Phi) (at level 50) : full_syntax.
Notation "∃ Phi" := (@quant _ _ full_operators _ Ex Phi) (at level 50) : full_syntax.
Notation "A ∧ B" := (@bin _ _ full_operators _ Conj A B) (at level 41) : full_syntax.
Notation "A ∨ B" := (@bin _ _ full_operators _ Disj A B) (at level 42) : full_syntax.
Notation "A → B" := (@bin _ _ full_operators _ Impl A B) (at level 43, right associativity) : full_syntax.
Notation "⊥" := (falsity) : full_syntax.
Notation "¬ A" := (A → ⊥) (at level 42) : full_syntax.
Notation "A ↔ B" := ((A → B) ∧ (B → A)) (at level 43) : full_syntax.
Fixpoint impl {Σ_funcs : funcs_signature} {Σ_preds : preds_signature} {ff : falsity_flag} (A : list form) phi :=
match A with
| [] => phi
| psi :: A => bin _ _ full_operators _ Impl psi (impl A phi)
end.
Notation "A ==> phi" := (impl A phi) (right associativity, at level 55).
Definition exist_times {Σ_funcs : funcs_signature} {Σ_preds : preds_signature} {ff : falsity_flag} n (phi : form) := iter (fun psi => ∃ psi) n phi.
Definition forall_times {Σ_funcs : funcs_signature} {Σ_preds : preds_signature} {ff : falsity_flag} n (phi : form) := iter (fun psi => ∀ psi) n phi.
End FullSyntax.
Module FragmentSyntax.
Inductive frag_logic_binop : Type :=
| Impl : frag_logic_binop.
Inductive frag_logic_quant : Type :=
| All : frag_logic_quant.
Definition frag_operators : operators :=
{| binop := frag_logic_binop ; quantop := frag_logic_quant |}.
#[export] Hint Immediate frag_operators : typeclass_instances.
Declare Scope fragment_syntax.
Delimit Scope fragment_syntax with Ffrag.
#[global] Open Scope fragment_syntax.
Notation "∀ Phi" := (@quant _ _ frag_operators _ All Phi) (at level 50) : fragment_syntax.
Notation "phi → psi" := (@bin _ _ frag_operators _ Impl phi psi) (at level 43, right associativity) : fragment_syntax.
Notation "¬ phi" := (phi → falsity) (at level 42) : fragment_syntax.
Notation "⊥" := (falsity) : fragment_syntax.
Fixpoint impl {Σ_funcs : funcs_signature} {Σ_preds : preds_signature} {ff : falsity_flag} (A : list form) phi :=
match A with
| [] => phi
| psi :: A => bin _ _ frag_operators _ Impl psi (impl A phi)
end.
Notation "A ==> phi" := (impl A phi) (right associativity, at level 55).
Definition forall_times {Σ_funcs : funcs_signature} {Σ_preds : preds_signature} {ff : falsity_flag} n (phi : form) := iter (fun psi => ∀ psi) n phi.
End FragmentSyntax.