From Equations Require Import Equations.
Require Equations.Type.DepElim.
From Undecidability.FOL Require Import Syntax.Core Deduction.FullND Semantics.Tarski.FullCore Arithmetics.PA.
From Undecidability.FOL.Proofmode Require Import Theories ProofMode.
Require Undecidability.FOL.Proofmode.Hoas.
Require Import String List.
Import ListNotations.
Open Scope string_scope.
Section FullLogic.
Existing Instance falsity_on.
Variable p : peirce.
Fixpoint num n :=
match n with
O => zero
| S x => σ (num x)
end.
Definition FAeq := ax_refl :: ax_sym :: ax_trans :: ax_succ_congr :: ax_add_congr :: ax_mult_congr :: ax_zero_succ :: FA.
Instance eqdec_funcs : EqDec PA_funcs_signature.
Proof. intros x y; decide equality. Qed.
Instance eqdec_preds : EqDec PA_preds_signature.
Proof. intros x y. destruct x, y. now left. Qed.
Ltac custom_fold ::= fold ax_induction in *.
Ltac custom_unfold ::= unfold ax_induction in *.
Goal forall a b c, nil ⊢ (a → (a → b) → (b → c) → c).
Proof.
intros. fstart. fintros. fapply "H1". fapply "H0". fapply "H".
Qed.
Lemma num_add_homomorphism x y :
FAeq ⊢ (num x ⊕ num y == num (x + y)).
Proof.
induction x; cbn.
- fapply ax_add_zero. - feapply ax_trans.
+ fapply ax_add_rec.
+ feapply ax_succ_congr. exact IHx.
Qed.
Lemma num_mult_homomorphism x y :
FAeq ⊢ ( num x ⊗ num y == num (x * y) ).
Proof.
induction x; cbn.
- fapply ax_mult_zero.
- feapply ax_trans.
+ feapply ax_trans.
* fapply ax_mult_rec.
* feapply ax_add_congr. fapply ax_refl. exact IHx.
+ apply num_add_homomorphism.
Qed.
Goal forall (φ : form), Qeq ⊢I ((∃φ[↑]) → φ)%Ffull.
Proof.
intros φ. fstart. Fail fintros "[z Hz]". fintros.
Fail fdestruct "H". Fail fdestruct "H" as "[x Hx]".
remember intu. fdestruct "H". ctx.
Qed.
Program Instance PA_Leibniz : Leibniz PA_funcs_signature PA_preds_signature falsity_on.
Next Obligation. exact Eq. Defined.
Next Obligation. exact FAeq. Defined.
Next Obligation. fintros. fapply ax_refl. Qed.
Next Obligation. fintros. fapply ax_sym. ctx. Qed.
Next Obligation.
unfold PA_Leibniz_obligation_1 in *. rename v1 into t; rename v2 into t0.
destruct F; repeat dependent elimination t0; repeat dependent elimination t.
- fapply ax_refl.
- fapply ax_succ_congr. apply H1.
- fapply ax_add_congr; apply H1.
- fapply ax_mult_congr; apply H1.
Qed.
Next Obligation.
unfold PA_Leibniz_obligation_1 in *. rename v1 into t; rename v2 into t0.
destruct P; repeat dependent elimination t0; repeat dependent elimination t.
- cbn in H1. split.
+ intros H2. feapply ax_trans. feapply ax_sym. apply H1. feapply ax_trans.
apply H2. apply H1.
+ intros H2. feapply ax_trans. apply H1. feapply ax_trans. apply H2.
fapply ax_sym. apply H1.
Qed.
Lemma num_add_homomorphism' x y :
FAeq ⊢ (num x ⊕ num y == num (x + y)).
Proof.
induction x; cbn.
- fapply ax_add_zero.
- frewrite <- IHx. fapply ax_add_rec.
Qed.
Lemma num_mult_homomorphism' x y :
FAeq ⊢ ( num x ⊗ num y == num (x * y) ).
Proof.
induction x; cbn.
- fapply ax_mult_zero.
- frewrite (ax_mult_rec (num x) (num y)). frewrite IHx. apply num_add_homomorphism'.
Qed.
Goal forall t t', FAeq ⊢ (t == t') -> FAeq ⊢ ∀ $0 ⊕ σ t`[↑] == t' ⊕ σ $0.
Proof.
intros. frewrite H.
Abort.
Goal forall t t', FAeq ⊢ (t == t') -> FAeq ⊢ ∀∃ $0 ⊕ σ t == t'`[↑]`[↑] ⊕ σ $0.
Proof.
intros. frewrite <- H.
Abort.
Goal forall phi, [] ⊢C (phi ∨ (phi → ⊥)).
Proof.
intro. fstart. fclassical phi.
- fleft. fapply "H".
- fright. fapply "H".
Qed.
Goal forall phi, [] ⊢C (((phi → ⊥) → ⊥) → phi).
Proof.
intro. fstart. fintros. fcontradict as "X". fapply "H". fapply "X".
Qed.
Import Hoas.
Notation "'σ' x" := (bFunc Succ (Vector.cons bterm x 0 (Vector.nil bterm))) (at level 32) : hoas_scope.
Notation "x '⊕' y" := (bFunc Plus (Vector.cons bterm x 1 (Vector.cons bterm y 0 (Vector.nil bterm))) ) (at level 39) : hoas_scope.
Notation "x '⊗' y" := (bFunc Mult (Vector.cons bterm x 1 (Vector.cons bterm y 0 (Vector.nil bterm))) ) (at level 38) : hoas_scope.
Notation "x '==' y" := (bAtom Eq (Vector.cons bterm x 1 (Vector.cons bterm y 0 (Vector.nil bterm))) ) (at level 40) : hoas_scope.
Open Scope PA_Notation.
Definition leq a b := (∃' k, a ⊕ k == b)%hoas.
Infix "≤" := leq (at level 45).
Definition FAI :=
ax_induction (<< Free x, ∀' y, (x == y) ∨ ¬ (x == y)) ::
ax_induction (<< Free x, zero == x ∨ ¬ (zero == x)) ::
(<< ∀' x, ax_induction (<< Free x y, (σ x == y) ∨ ¬ (σ x == y))) ::
ax_induction (<< Free x, ∀' y, ∃' q r, (x == r ⊕ q ⊗ σ y) ∧ (r ≤ y)) ::
ax_induction (<< Free k, ∀' r y, ¬ (r == y) → (r ⊕ k == y) → (∃' k', σ r ⊕ k' == y)) ::
ax_induction (<< Free x, ∀' y, x ⊕ σ y == σ (x ⊕ y)) ::
ax_induction (<< Free x, ∀' y, x ⊕ y == y ⊕ x) ::
ax_induction (<< Free x, x ⊕ zero == x) ::
ax_zero_succ ::
ax_succ_inj ::
FAeq.
Lemma add_zero_r :
FAI ⊢ << ∀' x, x ⊕ zero == x.
Proof.
fstart. fapply ((ax_induction (<< Free x, x ⊕ zero == x))).
- frewrite (ax_add_zero zero). fapply ax_refl.
- fintros "x" "IH". frewrite (ax_add_rec zero x). frewrite "IH". fapply ax_refl.
Qed.
Lemma add_succ_r :
FAI ⊢ << ∀' x y, x ⊕ σ y == σ (x ⊕ y).
Proof.
fstart. fapply ((ax_induction (<< Free x, ∀' y, x ⊕ σ y == σ (x ⊕ y)))).
- fintros "y". frewrite (ax_add_zero (σ y)). frewrite (ax_add_zero y). fapply ax_refl.
- fintros "x" "IH" "y". frewrite (ax_add_rec (σ y) x). frewrite ("IH" y).
frewrite (ax_add_rec y x). fapply ax_refl.
Qed.
Lemma add_comm :
FAI ⊢ << ∀' x y, x ⊕ y == y ⊕ x.
Proof.
fstart. fapply ((ax_induction (<< Free x, ∀' y, x ⊕ y == y ⊕ x))).
- fintros. frewrite (ax_add_zero x). frewrite (add_zero_r x). fapply ax_refl.
- fintros "x" "IH" "y". frewrite (add_succ_r y x). frewrite <- ("IH" y).
frewrite (ax_add_rec y x). fapply ax_refl.
Qed.
Lemma pa_eq_dec :
FAI ⊢ << ∀' x y, (x == y) ∨ ¬ (x == y).
Proof.
fstart. fapply ((ax_induction (<< Free x, ∀' y, (x == y) ∨ ¬ (x == y)))).
- fapply ((ax_induction (<< Free x, zero == x ∨ (zero == x → ⊥)))).
+ fleft. fapply ax_refl.
+ fintros "x" "IH". fright. fapply ax_zero_succ.
- fintros "x" "IH". fapply ((<< ∀' x, ax_induction (<< Free x y, (σ x == y) ∨ ¬ (σ x == y)))).
+ fright. fintros "H". feapply ax_zero_succ. feapply ax_sym. fapply "H".
+ fintros "y" "IHy". fspecialize ("IH" y). fdestruct "IH" as "[IH|IH]".
* fleft. frewrite "IH". fapply ax_refl.
* fright. fintros "H". fapply "IH". fapply ax_succ_inj. fapply "H".
Qed.
Lemma neq_le :
FAI ⊢ << ∀' k r y, ¬ (r == y) → (r ⊕ k == y) → ∃' k', σ r ⊕ k' == y.
Proof.
fstart. fapply ((ax_induction (<< Free k, ∀' r y, ¬ (r == y) → (r ⊕ k == y) → (∃' k', σ r ⊕ k' == y)))).
- fintros "r" "y" "H1" "H2". fexfalso. fapply "H1". frewrite <- (ax_add_zero r).
frewrite (add_comm zero r). ctx.
- fintros "k" "IH" "r" "y". fintros "H1" "H2". fexists k.
frewrite <- "H2". frewrite (ax_add_rec k r). frewrite (add_comm r (σ k)).
frewrite (ax_add_rec r k). frewrite (add_comm k r). fapply ax_refl.
Qed.
Lemma division_theorem :
FAI ⊢ << ∀' x y, ∃' q r, (x == r ⊕ q ⊗ σ y) ∧ (r ≤ y).
Proof.
fstart. fapply ((ax_induction (<< Free x, ∀' y, ∃' q r, (x == r ⊕ q ⊗ σ y) ∧ (r ≤ y)))).
- fintros "y". fexists zero. fexists zero. fsplit.
+ frewrite (ax_mult_zero (σ y)). frewrite (ax_add_zero zero). fapply ax_refl.
+ fexists y. fapply ax_add_zero.
- fintros "x" "IH" "y". fdestruct ("IH" y) as "[q [r [IH1 [k IH2]]]]".
fassert (<< r == y ∨ (r == y → ⊥)) as "[H|H]" by fapply pa_eq_dec.
+ fexists (σ q). fexists zero. fsplit.
* frewrite (ax_add_zero (σ q ⊗ σ y)). frewrite (ax_mult_rec q (σ y)).
frewrite (ax_add_rec (q ⊗ σ y) y). fapply ax_succ_congr.
frewrite "IH1". frewrite "H". fapply ax_refl.
* fexists y. fapply ax_add_zero.
+ fexists q. fexists (σ r). fsplit.
* frewrite (ax_add_rec (q ⊗ σ y) r). fapply ax_succ_congr. ctx.
* fapply (neq_le k r y); ctx.
Qed.
End FullLogic.
Require Equations.Type.DepElim.
From Undecidability.FOL Require Import Syntax.Core Deduction.FullND Semantics.Tarski.FullCore Arithmetics.PA.
From Undecidability.FOL.Proofmode Require Import Theories ProofMode.
Require Undecidability.FOL.Proofmode.Hoas.
Require Import String List.
Import ListNotations.
Open Scope string_scope.
Section FullLogic.
Existing Instance falsity_on.
Variable p : peirce.
Fixpoint num n :=
match n with
O => zero
| S x => σ (num x)
end.
Definition FAeq := ax_refl :: ax_sym :: ax_trans :: ax_succ_congr :: ax_add_congr :: ax_mult_congr :: ax_zero_succ :: FA.
Instance eqdec_funcs : EqDec PA_funcs_signature.
Proof. intros x y; decide equality. Qed.
Instance eqdec_preds : EqDec PA_preds_signature.
Proof. intros x y. destruct x, y. now left. Qed.
Ltac custom_fold ::= fold ax_induction in *.
Ltac custom_unfold ::= unfold ax_induction in *.
Goal forall a b c, nil ⊢ (a → (a → b) → (b → c) → c).
Proof.
intros. fstart. fintros. fapply "H1". fapply "H0". fapply "H".
Qed.
Lemma num_add_homomorphism x y :
FAeq ⊢ (num x ⊕ num y == num (x + y)).
Proof.
induction x; cbn.
- fapply ax_add_zero. - feapply ax_trans.
+ fapply ax_add_rec.
+ feapply ax_succ_congr. exact IHx.
Qed.
Lemma num_mult_homomorphism x y :
FAeq ⊢ ( num x ⊗ num y == num (x * y) ).
Proof.
induction x; cbn.
- fapply ax_mult_zero.
- feapply ax_trans.
+ feapply ax_trans.
* fapply ax_mult_rec.
* feapply ax_add_congr. fapply ax_refl. exact IHx.
+ apply num_add_homomorphism.
Qed.
Goal forall (φ : form), Qeq ⊢I ((∃φ[↑]) → φ)%Ffull.
Proof.
intros φ. fstart. Fail fintros "[z Hz]". fintros.
Fail fdestruct "H". Fail fdestruct "H" as "[x Hx]".
remember intu. fdestruct "H". ctx.
Qed.
Program Instance PA_Leibniz : Leibniz PA_funcs_signature PA_preds_signature falsity_on.
Next Obligation. exact Eq. Defined.
Next Obligation. exact FAeq. Defined.
Next Obligation. fintros. fapply ax_refl. Qed.
Next Obligation. fintros. fapply ax_sym. ctx. Qed.
Next Obligation.
unfold PA_Leibniz_obligation_1 in *. rename v1 into t; rename v2 into t0.
destruct F; repeat dependent elimination t0; repeat dependent elimination t.
- fapply ax_refl.
- fapply ax_succ_congr. apply H1.
- fapply ax_add_congr; apply H1.
- fapply ax_mult_congr; apply H1.
Qed.
Next Obligation.
unfold PA_Leibniz_obligation_1 in *. rename v1 into t; rename v2 into t0.
destruct P; repeat dependent elimination t0; repeat dependent elimination t.
- cbn in H1. split.
+ intros H2. feapply ax_trans. feapply ax_sym. apply H1. feapply ax_trans.
apply H2. apply H1.
+ intros H2. feapply ax_trans. apply H1. feapply ax_trans. apply H2.
fapply ax_sym. apply H1.
Qed.
Lemma num_add_homomorphism' x y :
FAeq ⊢ (num x ⊕ num y == num (x + y)).
Proof.
induction x; cbn.
- fapply ax_add_zero.
- frewrite <- IHx. fapply ax_add_rec.
Qed.
Lemma num_mult_homomorphism' x y :
FAeq ⊢ ( num x ⊗ num y == num (x * y) ).
Proof.
induction x; cbn.
- fapply ax_mult_zero.
- frewrite (ax_mult_rec (num x) (num y)). frewrite IHx. apply num_add_homomorphism'.
Qed.
Goal forall t t', FAeq ⊢ (t == t') -> FAeq ⊢ ∀ $0 ⊕ σ t`[↑] == t' ⊕ σ $0.
Proof.
intros. frewrite H.
Abort.
Goal forall t t', FAeq ⊢ (t == t') -> FAeq ⊢ ∀∃ $0 ⊕ σ t == t'`[↑]`[↑] ⊕ σ $0.
Proof.
intros. frewrite <- H.
Abort.
Goal forall phi, [] ⊢C (phi ∨ (phi → ⊥)).
Proof.
intro. fstart. fclassical phi.
- fleft. fapply "H".
- fright. fapply "H".
Qed.
Goal forall phi, [] ⊢C (((phi → ⊥) → ⊥) → phi).
Proof.
intro. fstart. fintros. fcontradict as "X". fapply "H". fapply "X".
Qed.
Import Hoas.
Notation "'σ' x" := (bFunc Succ (Vector.cons bterm x 0 (Vector.nil bterm))) (at level 32) : hoas_scope.
Notation "x '⊕' y" := (bFunc Plus (Vector.cons bterm x 1 (Vector.cons bterm y 0 (Vector.nil bterm))) ) (at level 39) : hoas_scope.
Notation "x '⊗' y" := (bFunc Mult (Vector.cons bterm x 1 (Vector.cons bterm y 0 (Vector.nil bterm))) ) (at level 38) : hoas_scope.
Notation "x '==' y" := (bAtom Eq (Vector.cons bterm x 1 (Vector.cons bterm y 0 (Vector.nil bterm))) ) (at level 40) : hoas_scope.
Open Scope PA_Notation.
Definition leq a b := (∃' k, a ⊕ k == b)%hoas.
Infix "≤" := leq (at level 45).
Definition FAI :=
ax_induction (<< Free x, ∀' y, (x == y) ∨ ¬ (x == y)) ::
ax_induction (<< Free x, zero == x ∨ ¬ (zero == x)) ::
(<< ∀' x, ax_induction (<< Free x y, (σ x == y) ∨ ¬ (σ x == y))) ::
ax_induction (<< Free x, ∀' y, ∃' q r, (x == r ⊕ q ⊗ σ y) ∧ (r ≤ y)) ::
ax_induction (<< Free k, ∀' r y, ¬ (r == y) → (r ⊕ k == y) → (∃' k', σ r ⊕ k' == y)) ::
ax_induction (<< Free x, ∀' y, x ⊕ σ y == σ (x ⊕ y)) ::
ax_induction (<< Free x, ∀' y, x ⊕ y == y ⊕ x) ::
ax_induction (<< Free x, x ⊕ zero == x) ::
ax_zero_succ ::
ax_succ_inj ::
FAeq.
Lemma add_zero_r :
FAI ⊢ << ∀' x, x ⊕ zero == x.
Proof.
fstart. fapply ((ax_induction (<< Free x, x ⊕ zero == x))).
- frewrite (ax_add_zero zero). fapply ax_refl.
- fintros "x" "IH". frewrite (ax_add_rec zero x). frewrite "IH". fapply ax_refl.
Qed.
Lemma add_succ_r :
FAI ⊢ << ∀' x y, x ⊕ σ y == σ (x ⊕ y).
Proof.
fstart. fapply ((ax_induction (<< Free x, ∀' y, x ⊕ σ y == σ (x ⊕ y)))).
- fintros "y". frewrite (ax_add_zero (σ y)). frewrite (ax_add_zero y). fapply ax_refl.
- fintros "x" "IH" "y". frewrite (ax_add_rec (σ y) x). frewrite ("IH" y).
frewrite (ax_add_rec y x). fapply ax_refl.
Qed.
Lemma add_comm :
FAI ⊢ << ∀' x y, x ⊕ y == y ⊕ x.
Proof.
fstart. fapply ((ax_induction (<< Free x, ∀' y, x ⊕ y == y ⊕ x))).
- fintros. frewrite (ax_add_zero x). frewrite (add_zero_r x). fapply ax_refl.
- fintros "x" "IH" "y". frewrite (add_succ_r y x). frewrite <- ("IH" y).
frewrite (ax_add_rec y x). fapply ax_refl.
Qed.
Lemma pa_eq_dec :
FAI ⊢ << ∀' x y, (x == y) ∨ ¬ (x == y).
Proof.
fstart. fapply ((ax_induction (<< Free x, ∀' y, (x == y) ∨ ¬ (x == y)))).
- fapply ((ax_induction (<< Free x, zero == x ∨ (zero == x → ⊥)))).
+ fleft. fapply ax_refl.
+ fintros "x" "IH". fright. fapply ax_zero_succ.
- fintros "x" "IH". fapply ((<< ∀' x, ax_induction (<< Free x y, (σ x == y) ∨ ¬ (σ x == y)))).
+ fright. fintros "H". feapply ax_zero_succ. feapply ax_sym. fapply "H".
+ fintros "y" "IHy". fspecialize ("IH" y). fdestruct "IH" as "[IH|IH]".
* fleft. frewrite "IH". fapply ax_refl.
* fright. fintros "H". fapply "IH". fapply ax_succ_inj. fapply "H".
Qed.
Lemma neq_le :
FAI ⊢ << ∀' k r y, ¬ (r == y) → (r ⊕ k == y) → ∃' k', σ r ⊕ k' == y.
Proof.
fstart. fapply ((ax_induction (<< Free k, ∀' r y, ¬ (r == y) → (r ⊕ k == y) → (∃' k', σ r ⊕ k' == y)))).
- fintros "r" "y" "H1" "H2". fexfalso. fapply "H1". frewrite <- (ax_add_zero r).
frewrite (add_comm zero r). ctx.
- fintros "k" "IH" "r" "y". fintros "H1" "H2". fexists k.
frewrite <- "H2". frewrite (ax_add_rec k r). frewrite (add_comm r (σ k)).
frewrite (ax_add_rec r k). frewrite (add_comm k r). fapply ax_refl.
Qed.
Lemma division_theorem :
FAI ⊢ << ∀' x y, ∃' q r, (x == r ⊕ q ⊗ σ y) ∧ (r ≤ y).
Proof.
fstart. fapply ((ax_induction (<< Free x, ∀' y, ∃' q r, (x == r ⊕ q ⊗ σ y) ∧ (r ≤ y)))).
- fintros "y". fexists zero. fexists zero. fsplit.
+ frewrite (ax_mult_zero (σ y)). frewrite (ax_add_zero zero). fapply ax_refl.
+ fexists y. fapply ax_add_zero.
- fintros "x" "IH" "y". fdestruct ("IH" y) as "[q [r [IH1 [k IH2]]]]".
fassert (<< r == y ∨ (r == y → ⊥)) as "[H|H]" by fapply pa_eq_dec.
+ fexists (σ q). fexists zero. fsplit.
* frewrite (ax_add_zero (σ q ⊗ σ y)). frewrite (ax_mult_rec q (σ y)).
frewrite (ax_add_rec (q ⊗ σ y) y). fapply ax_succ_congr.
frewrite "IH1". frewrite "H". fapply ax_refl.
* fexists y. fapply ax_add_zero.
+ fexists q. fexists (σ r). fsplit.
* frewrite (ax_add_rec (q ⊗ σ y) r). fapply ax_succ_congr. ctx.
* fapply (neq_le k r y); ctx.
Qed.
End FullLogic.