From Loeb Require Import Definitions.
From Loeb.util Require Import Util.
From Loeb.internal_provability Require Import PA_Lists_Signature QEqLiFull.
From Loeb.hilbert_system Require Import Hilbert_System.
From Undecidability.FOL Require Import Syntax.Core Arithmetics.Signature Arithmetics.FA Arithmetics.Robinson.
From FOL.Proofmode Require Import Theories ProofMode.
From FOL.Incompleteness Require Import utils.
Require FOL.Proofmode.Hoas.
Require Import Lia.
From Equations Require Import Equations.
Require Import String List.
From Loeb.util Require Import Util.
From Loeb.internal_provability Require Import PA_Lists_Signature QEqLiFull.
From Loeb.hilbert_system Require Import Hilbert_System.
From Undecidability.FOL Require Import Syntax.Core Arithmetics.Signature Arithmetics.FA Arithmetics.Robinson.
From FOL.Proofmode Require Import Theories ProofMode.
From FOL.Incompleteness Require Import utils.
Require FOL.Proofmode.Hoas.
Require Import Lia.
From Equations Require Import Equations.
Require Import String List.
Section DefProv.
Existing Instance falsity_on.
Existing Instance PA_li_funcs_signature.
Existing Instance PA_preds_signature.
Existing Instance full_operators.
Open Scope PA_li_Notation.
Variables pei: peirce.
Variables göd: goedelisation.
Existing Instance falsity_on.
Existing Instance PA_li_funcs_signature.
Existing Instance PA_preds_signature.
Existing Instance full_operators.
Open Scope PA_li_Notation.
Variables pei: peirce.
Variables göd: goedelisation.
Variables ax: form.
Variables ax_bound: bounded 1 ax.
Variables Hax: forall φ, (QEqLiFull φ \/ exists n ψ, hilAx pei ψ /\ φ = forall_times n ψ) <-> QEqLi ⊢ ax[(num' ((göd.(g)) φ))..].
Definition well_formed := ax[($1 G $0)..] ∨ ∃∃ $0 ⧀l $2 ∧ $1 ⧀l $2 ∧ (($3 G $0) === (($3 G $1) ~> ($3 G $2))).
Definition prf := (∃ σ $0 === len $2 ∧ ($2 G $0) === $1) ∧ ∀ $0 ⧀l len $2 → well_formed[$0 .: $2..].
Definition prov := ∃ prf [$1 .: $0..].
Lemma bound_un_fun (t1: term) (k: nat):
bounded_t k t1 -> forall t : term, Vector.In t (Vector.cons term t1 0 (Vector.nil term)) -> bounded_t k t.
Proof.
intros Ht1 t Ht. apply In_inv in Ht as [Hd | Htl].
- cbn in Hd. rewrite Hd. assumption.
- exfalso. apply (In_inv Htl).
Qed.
Lemma bound_bin_fun (t1 t2: term) (k: nat):
bounded_t k t1 -> bounded_t k t2 -> forall t : term, Vector.In t (Vector.cons term t1 1 (Vector.cons term t2 0 (Vector.nil term))) -> bounded_t k t.
Proof.
intros Ht1 Ht2 t Ht. apply In_inv in Ht as [Hd | Htl].
- cbn in Hd. rewrite Hd. assumption.
- apply In_inv in Htl as [Hd | Htl].
+ cbn in Hd. rewrite Hd. assumption.
+ cbn in Htl. exfalso. apply (In_inv Htl).
Qed.
Lemma well_formed_bound:
bounded 2 well_formed.
Proof.
unfold well_formed. constructor.
- eapply subst_bounded_max; last exact ax_bound. intros [| k] Hk; last lia. cbn.
constructor. apply bound_bin_fun; constructor; lia.
- repeat constructor.
+ apply bound_bin_fun.
* cbn. constructor. lia.
* cbn. constructor. apply bound_bin_fun; last (constructor; lia). constructor. apply bound_un_fun. constructor. lia.
+ apply bound_bin_fun; cbn; first (constructor; lia). constructor. apply bound_bin_fun; last (constructor; lia).
constructor. apply bound_un_fun. constructor. lia.
+ apply bound_bin_fun.
* constructor. apply bound_bin_fun; constructor; lia.
* constructor. apply bound_bin_fun; constructor; apply bound_bin_fun; constructor; lia.
Qed.
Instance eqdec_funcs: EqDec PA_li_funcs_signature.
Proof. intros x y. apply PA_li_funcs_eq. Qed.
Instance eqdec_preds : EqDec PA_preds_signature.
Proof. intros x y. destruct x, y. now left. Qed.
Open Scope string_scope.
Opaque QEqLi.
Existing Instance PA_li_Leibniz.
bounded_t k t1 -> forall t : term, Vector.In t (Vector.cons term t1 0 (Vector.nil term)) -> bounded_t k t.
Proof.
intros Ht1 t Ht. apply In_inv in Ht as [Hd | Htl].
- cbn in Hd. rewrite Hd. assumption.
- exfalso. apply (In_inv Htl).
Qed.
Lemma bound_bin_fun (t1 t2: term) (k: nat):
bounded_t k t1 -> bounded_t k t2 -> forall t : term, Vector.In t (Vector.cons term t1 1 (Vector.cons term t2 0 (Vector.nil term))) -> bounded_t k t.
Proof.
intros Ht1 Ht2 t Ht. apply In_inv in Ht as [Hd | Htl].
- cbn in Hd. rewrite Hd. assumption.
- apply In_inv in Htl as [Hd | Htl].
+ cbn in Hd. rewrite Hd. assumption.
+ cbn in Htl. exfalso. apply (In_inv Htl).
Qed.
Lemma well_formed_bound:
bounded 2 well_formed.
Proof.
unfold well_formed. constructor.
- eapply subst_bounded_max; last exact ax_bound. intros [| k] Hk; last lia. cbn.
constructor. apply bound_bin_fun; constructor; lia.
- repeat constructor.
+ apply bound_bin_fun.
* cbn. constructor. lia.
* cbn. constructor. apply bound_bin_fun; last (constructor; lia). constructor. apply bound_un_fun. constructor. lia.
+ apply bound_bin_fun; cbn; first (constructor; lia). constructor. apply bound_bin_fun; last (constructor; lia).
constructor. apply bound_un_fun. constructor. lia.
+ apply bound_bin_fun.
* constructor. apply bound_bin_fun; constructor; lia.
* constructor. apply bound_bin_fun; constructor; apply bound_bin_fun; constructor; lia.
Qed.
Instance eqdec_funcs: EqDec PA_li_funcs_signature.
Proof. intros x y. apply PA_li_funcs_eq. Qed.
Instance eqdec_preds : EqDec PA_preds_signature.
Proof. intros x y. destruct x, y. now left. Qed.
Open Scope string_scope.
Opaque QEqLi.
Existing Instance PA_li_Leibniz.
Lemma singleton_list_access:
QEqLi ⊢ ∀∀ $0 ⧀l (len ($1 ::: [|])) → (($1 ::: [|]) G $0) === $1.
Proof.
fstart. fintros "x" "i" "[k Hk]". fassert (σ zero === σ i ⊕ k) as "Hi".
frewrite <- "Hk". frewrite (ax_len_cons [|] x).
fassert (len [|] === zero) as "->". fapply ax_len_nil.
fapply ((form_inclusion ax_refl)).
fassert (zero === i ⊕ k) as "Hzero". fapply ((form_inclusion ax_succ_inj)).
frewrite <- ((form_inclusion ax_add_rec) k i). fapply "Hi".
fassert (∀ $0 === zero ∨ ∃ $1 === σ $0) as "Hcases".
fintros "j". fapply ((form_inclusion ax_cases)).
fdestruct ("Hcases" i) as "[HiZero|[j Hj]]".
- frewrite "HiZero". fapply ax_get_zero.
- fexfalso. fapply ((form_inclusion ax_zero_succ) (j ⊕ k)).
frewrite <- ((form_inclusion ax_add_rec) k j). frewrite <- "Hj".
fapply "Hzero".
Qed.
Lemma axioms_are_provable φ:
QEqLi ⊢ ax[(num' ((göd.(g)) φ))..] -> QEqLiFull ⊩ (prov[(num' (g φ))..]).
Proof.
intros HaxDeriv. fstart. exists QEqLi. split.
- intros ψ Hψ. constructor. assumption.
- fstart. unfold prov. asimpl. pose (p := num' (g φ)); fold p. fexists (p:::[|]).
fsplit.
+ fexists zero. fassert (len (p ::: [|]) === σ (len [|])) as "->".
fapply ax_len_cons. fassert (len [|] === zero) as "->". fapply ax_len_nil. fassert (((p ::: [|]) G zero) === p) as "->". fapply ax_get_zero.
fsplit; fapply ((∀ $0 === $0)).
+ fintros i "Hi". fleft. asimpl. replace (ax[_]) with (ax[((p ::: [|]) G i)..]).
2: { apply subst_bound_1. assumption. }
fassert (((p ::: [|]) G i) === p) as "Hp".
fapply singleton_list_access. fapply "Hi".
feapply QEqLi_leibniz; last feapply HaxDeriv. fold p.
frewrite "Hp". fapply ((∀ $0 === $0)).
Qed.
AxiomList is needed in order to use the proofmode on finite context instead of infinite theores
This is because rewriting is not supported for infinite theories.
Definition AxiomList := (ax_induction' ($0 === $0 ⊕ zero))::
(ax_induction' (∀ $1 ⊕ σ $0 === σ ($1 ⊕ $0)))::
(ax_induction' (∀ $0 ⊕ $1 === $1 ⊕ $0))::
(ax_induction' (∀∀ $2 === σ (($2 ⊕ $1) ⊕ $0) → ⊥))::
(ax_induction' (∀∀ ($0 ⊕ $1) ⊕ $2 === $0 ⊕ ($1 ⊕ $2)))::
(ax_induction' (∀ $0 ⧀l $1 ∨ $1 ⧀l $0 ∨ $1 === $0))::
(ax_induction' (∀∀ $2 ⊕ $0 === $2 ⊕ $1 → $0 === $1))::
QEqLi.
(ax_induction' (∀ $1 ⊕ σ $0 === σ ($1 ⊕ $0)))::
(ax_induction' (∀ $0 ⊕ $1 === $1 ⊕ $0))::
(ax_induction' (∀∀ $2 === σ (($2 ⊕ $1) ⊕ $0) → ⊥))::
(ax_induction' (∀∀ ($0 ⊕ $1) ⊕ $2 === $0 ⊕ ($1 ⊕ $2)))::
(ax_induction' (∀ $0 ⧀l $1 ∨ $1 ⧀l $0 ∨ $1 === $0))::
(ax_induction' (∀∀ $2 ⊕ $0 === $2 ⊕ $1 → $0 === $1))::
QEqLi.
All elements of the AxiomList are indeed axioms of QEqLiFull
Lemma AxiomList_in_QEqLi_Axioms:
forall φ, In φ AxiomList -> QEqLiFull φ.
Proof.
Opaque QEqLi.
intros φ Hφ. unfold AxiomList in Hφ. cbn in Hφ.
decompose [or] Hφ; last now apply In_QEqLi.
all: subst φ; now apply QEqInduction.
Transparent QEqLi.
Qed.
Lemma x_plus_zero (p: peirce):
AxiomList ⊢ ∀ $0 === $0 ⊕ zero.
Proof.
fstart. unfold AxiomList. unfold ax_induction'. fapply 0.
- frewrite ((form_inclusion ax_add_zero) zero). fapply ((form_inclusion ax_refl)).
- fintros x "IH". frewrite ((form_inclusion ax_add_rec) zero x).
frewrite <- "IH". fapply ((form_inclusion ax_refl)).
Qed.
Lemma add_rec_right (p: peirce):
AxiomList ⊢ ∀∀ $1 ⊕ σ $0 === σ ($1 ⊕ $0).
Proof.
fstart. unfold AxiomList. unfold ax_induction'. fapply 1.
- fintros y. frewrite ((form_inclusion ax_add_zero) (σ y)).
frewrite ((form_inclusion ax_add_zero) y). fapply ((form_inclusion ax_refl)).
- fintros x "IH". fintros y. frewrite ((form_inclusion ax_add_rec) (σ y) x).
frewrite ((form_inclusion ax_add_rec) y x). frewrite ("IH" y).
fapply ((form_inclusion ax_refl)).
Qed.
Lemma add_comm (p: peirce):
AxiomList ⊢ ∀∀ $0 ⊕ $1 === $1 ⊕ $0.
Proof.
fstart. unfold AxiomList. unfold ax_induction'. fapply 2.
- fintros y. frewrite <- (x_plus_zero y). frewrite ((form_inclusion ax_add_zero) y).
fapply ((form_inclusion ax_refl)).
- fintros x "IH". fintros y. frewrite (add_rec_right y x).
frewrite ((form_inclusion ax_add_rec) y x). frewrite ("IH" y).
fapply ((form_inclusion ax_refl)).
Qed.
Lemma add_one (p: peirce):
AxiomList ⊢ ∀∀ σ ($0 ⊕ $1) === ($0 ⊕ $1) ⊕ σ zero.
Proof.
fstart. fintros "x" "y". fassert ((y ⊕ x) ⊕ σ zero === σ ((y ⊕ x) ⊕ zero)) as "->".
fapply add_rec_right.
fassert (y ⊕ x === (y ⊕ x) ⊕ zero) as "<-".
fapply x_plus_zero. fapply ((form_inclusion ax_refl)).
Qed.
Lemma σ_large_injective (p: peirce):
AxiomList ⊢ ∀∀∀ $2 === σ (($2 ⊕ $1) ⊕ $0) → ⊥.
Proof.
fstart. unfold AxiomList. unfold ax_induction'. fapply 3.
- fintros "k" "k'". fapply ((form_inclusion ax_zero_succ)).
- fintros "x" "IH" "k" "k'". fintros "H".
fapply ("IH" k k'). frewrite <- ((form_inclusion ax_add_rec) k' (x ⊕ k)).
frewrite <- ((form_inclusion ax_add_rec) k x).
fapply ((form_inclusion ax_succ_inj)). fapply "H".
Qed.
Lemma add_assoc (p: peirce):
AxiomList ⊢ ∀∀∀ ($0 ⊕ $1) ⊕ $2 === $0 ⊕ ($1 ⊕ $2).
Proof.
fstart. unfold AxiomList. unfold ax_induction'. fapply 4.
- fintros "y" "x". frewrite <- (x_plus_zero y).
frewrite <- (x_plus_zero (x ⊕ y)). fapply ((form_inclusion ax_refl)).
- fintros "z" "IH" "y" "x". frewrite (add_rec_right y z).
frewrite (add_rec_right (x ⊕ y) z). frewrite (add_rec_right x (y ⊕ z)).
fapply ((form_inclusion ax_succ_congr)). fapply "IH".
Qed.
Lemma ineq_sandwich (p: peirce):
AxiomList ⊢ ∀∀ $1 ⧀l $0 → $0 ⧀l σ $1 → ⊥.
Proof.
fstart. fintros "x" "y" "[k Hk]" "[k' Hk']".
fassert (x === σ (x ⊕ k) ⊕ k') as "Hx".
fapply ((form_inclusion ax_succ_inj)). frewrite <- ((form_inclusion ax_add_rec) k x).
frewrite <- "Hk". frewrite <- ((form_inclusion ax_add_rec) k' y). fapply "Hk'".
fapply (σ_large_injective x k k'). frewrite <- ((form_inclusion ax_add_rec) k' (x ⊕ k)).
fapply "Hx".
Qed.
Lemma less_by_one (p: peirce):
AxiomList ⊢ ∀∀ σ $0 === $1 → $0 ⧀l $1.
Proof.
fstart. fintros "a" "b" "Hab". fexists zero.
frewrite "Hab". fapply x_plus_zero.
Qed.
Lemma ineq_plus (p: peirce):
AxiomList ⊢ ∀∀∀ $0 ⧀l $1 → $2 ⊕ $0 ⧀l $2 ⊕ $1.
Proof.
fstart. fintros "k" "y" "x" "[k' Hk']". fexists k'. frewrite "Hk'".
frewrite ((form_inclusion ax_add_rec) k' (k ⊕ x)).
frewrite ((form_inclusion ax_add_rec) k' x). frewrite (add_rec_right k (x ⊕ k')).
fapply ((form_inclusion ax_succ_congr)). frewrite (add_assoc k' x k).
fapply ((form_inclusion ax_refl)).
Qed.
Lemma ineq_dec (p: peirce):
AxiomList ⊢ ∀∀ $0 ⧀l $1 ∨ $1 ⧀l $0 ∨ $1 === $0.
Proof.
fstart. unfold AxiomList. unfold ax_induction'. fapply 5.
- fintros "y". fassert (y === zero ∨ ∃ y`[↑] === σ $0) as "[Heq|[k Hk]]".
fapply ((form_inclusion ax_cases)).
+ fright. fapply ((form_inclusion ax_sym)). fapply "Heq".
+ fleft. fright. fexists k. frewrite ((form_inclusion ax_add_rec) k zero).
frewrite ((form_inclusion ax_add_zero) k). fapply "Hk".
- fintros "x" "IH" "y". fassert (y === zero ∨ ∃ y`[↑] === σ $0) as "[Heq|[y' Hy']]".
fapply ((form_inclusion ax_cases)).
+ fleft. fleft. fexists x. frewrite "Heq".
frewrite ((form_inclusion ax_add_rec) x zero).
frewrite ((form_inclusion ax_add_zero) x). fapply ((form_inclusion ax_refl)).
+ fdestruct ("IH" y') as "[[[k Hk]|[k Hk]]|Heq]".
* fleft. fleft. fexists k. frewrite "Hy'".
frewrite ((form_inclusion ax_add_rec) k (σ y')).
fapply ((form_inclusion ax_succ_congr)). fapply "Hk".
* fleft. fright. fexists k. frewrite "Hy'".
frewrite ((form_inclusion ax_add_rec) k (σ x)).
fapply ((form_inclusion ax_succ_congr)). fapply "Hk".
* fright. frewrite "Heq". frewrite "Hy'".
fapply ((form_inclusion ax_refl)).
Qed.
Lemma ineq_trans (p: peirce):
AxiomList ⊢ ∀∀∀ $0 ⧀l $1 → $1 ⧀l $2 → $0 ⧀l $2.
Proof.
fstart. fintros "z" "y" "x". fintros "[k Hk]" "[k' Hk']".
fexists (k ⊕ σ k'). fassert ((σ x ⊕ k) ⊕ σ k' === σ x ⊕ (k ⊕ σ k')) as "<-". fapply add_assoc. frewrite <- "Hk".
fassert (y ⊕ σ k' === σ (y ⊕ k')) as "->". fapply add_rec_right.
frewrite <- ((form_inclusion ax_add_rec) k' y). fapply "Hk'".
Qed.
Lemma len_app_plus_one (p: peirce):
AxiomList ⊢ ∀∀∀ σ (len $0 ⊕ len $1) === len (($0 +++ $1) +++ ($2 ::: [|])).
Proof.
fstart. fintros "t2" "y" "x".
fassert (∀∀ len ($0 +++ $1) === len $0 ⊕ len $1) as "Hax_len_app".
fintros "a" "b". fapply ax_len_app.
fassert (∀∀ len ($0 ::: $1) === σ (len $1)) as "Hax_len_cons".
fintros "a" "b". fapply ax_len_cons.
fassert (len [|] === zero) as "Hax_len_nil".
fapply ax_len_nil.
frewrite ("Hax_len_app" (t2 ::: [|]) (x +++ y)). frewrite ("Hax_len_app" y x).
frewrite ("Hax_len_cons" [|] t2). frewrite "Hax_len_nil". fapply add_one.
Qed.
Lemma len_app_ineq (p: peirce):
AxiomList ⊢ ∀∀∀ $0 ⧀l len $1 → $0 ⧀l len ($1 +++ $2).
Proof.
fstart. fintros "y" "x" "i" "[k Hk]".
fexists (k ⊕ len y). frewrite (ax_len_app y x).
fassert ((σ i ⊕ k) ⊕ len y === σ i ⊕ (k ⊕ len y)) as "<-". fapply add_assoc.
frewrite <- "Hk". fapply ((form_inclusion ax_refl)).
Qed.
Lemma len_app_ineq' (p: peirce):
AxiomList ⊢ ∀∀∀ $0 ⧀l len $2 → len $1 ⊕ $0 ⧀l len ($1 +++ $2).
Proof.
fstart. fintros "y" "x" "i" "[k Hk]". fexists k.
frewrite (ax_len_app y x). fassert (len x ⊕ σ i === σ (len x ⊕ i)) as "<-". fapply add_rec_right. frewrite (add_assoc k (σ i) (len x)).
frewrite <- "Hk". fapply ((form_inclusion ax_refl)).
Qed.
Lemma get_low_index' (p: peirce):
AxiomList ⊢ ∀∀∀∀ $0 ⧀l len $1 → ((($1 +++ $2) +++ $3) G $0) === ($1 G $0).
Proof.
fstart. fintros "z" "y" "x" "i". fintros "Hi".
fassert (((x +++ y) +++ z G i) === ((x +++ y) G i)) as "->".
fapply ax_get_app_left. fapply len_app_ineq. fapply "Hi".
fapply ax_get_app_left. fapply "Hi".
Qed.
Lemma get_low_index (p: peirce):
AxiomList ⊢ ∀∀∀∀∀ $0 ⧀l $1 → $1 ⧀l len $2 → ((($2 +++ $3) +++ $4) G $0) === ($2 G $0).
Proof.
fstart. fintros "z" "y" "x" "j". fintros "i" "Hj" "Hi".
fassert (i ⧀l len x) as "Hi'". feapply ineq_trans. feapply "Hj". fapply "Hi".
fapply get_low_index'. fapply "Hi'".
Qed.
Lemma get_mid_index' (p: peirce):
AxiomList ⊢ ∀∀∀∀ $0 ⧀l len $2 → ((($1 +++ $2) +++ $3) G (len $1 ⊕ $0)) === ($2 G $0).
Proof.
fstart. fintros "z" "y" "x" "i". fintros "Hi".
fassert (((x +++ y) +++ z G (len x ⊕ i)) === ((x +++ y) G (len x ⊕ i))) as "->".
fapply ax_get_app_left. fapply len_app_ineq'. fapply "Hi".
frewrite (add_comm i (len x)). fapply ax_get_app_right. fapply "Hi".
Qed.
Lemma get_mid_index (p: peirce):
AxiomList ⊢ ∀∀∀∀∀ $0 ⧀l $1 → $1 ⧀l len $3 → ((($2 +++ $3) +++ $4) G (len $2 ⊕ $0)) === ($3 G $0).
Proof.
fstart. fintros "t2" "y" "x" "j". fintros "i" "Hj" "Hi".
fassert (i ⧀l len y) as "Hi'". feapply ineq_trans. feapply "Hj". feapply "Hi".
fapply get_mid_index'. fapply "Hi'".
Qed.
Lemma add_cancel (p: peirce):
AxiomList ⊢ ∀∀∀ $2 ⊕ $0 === $2 ⊕ $1 → $0 === $1.
Proof.
fstart. unfold AxiomList. unfold ax_induction'. fapply 6.
- fintros "z" "y". frewrite ((form_inclusion ax_add_zero) y).
frewrite ((form_inclusion ax_add_zero) z). fintros "H"; fapply "H".
- fintros "x" "IH" "z" "y". frewrite ((form_inclusion ax_add_rec) y x).
frewrite ((form_inclusion ax_add_rec) z x). fintros "H". fapply "IH".
fapply ((form_inclusion ax_succ_inj)). fapply "H".
Qed.
forall φ, In φ AxiomList -> QEqLiFull φ.
Proof.
Opaque QEqLi.
intros φ Hφ. unfold AxiomList in Hφ. cbn in Hφ.
decompose [or] Hφ; last now apply In_QEqLi.
all: subst φ; now apply QEqInduction.
Transparent QEqLi.
Qed.
Lemma x_plus_zero (p: peirce):
AxiomList ⊢ ∀ $0 === $0 ⊕ zero.
Proof.
fstart. unfold AxiomList. unfold ax_induction'. fapply 0.
- frewrite ((form_inclusion ax_add_zero) zero). fapply ((form_inclusion ax_refl)).
- fintros x "IH". frewrite ((form_inclusion ax_add_rec) zero x).
frewrite <- "IH". fapply ((form_inclusion ax_refl)).
Qed.
Lemma add_rec_right (p: peirce):
AxiomList ⊢ ∀∀ $1 ⊕ σ $0 === σ ($1 ⊕ $0).
Proof.
fstart. unfold AxiomList. unfold ax_induction'. fapply 1.
- fintros y. frewrite ((form_inclusion ax_add_zero) (σ y)).
frewrite ((form_inclusion ax_add_zero) y). fapply ((form_inclusion ax_refl)).
- fintros x "IH". fintros y. frewrite ((form_inclusion ax_add_rec) (σ y) x).
frewrite ((form_inclusion ax_add_rec) y x). frewrite ("IH" y).
fapply ((form_inclusion ax_refl)).
Qed.
Lemma add_comm (p: peirce):
AxiomList ⊢ ∀∀ $0 ⊕ $1 === $1 ⊕ $0.
Proof.
fstart. unfold AxiomList. unfold ax_induction'. fapply 2.
- fintros y. frewrite <- (x_plus_zero y). frewrite ((form_inclusion ax_add_zero) y).
fapply ((form_inclusion ax_refl)).
- fintros x "IH". fintros y. frewrite (add_rec_right y x).
frewrite ((form_inclusion ax_add_rec) y x). frewrite ("IH" y).
fapply ((form_inclusion ax_refl)).
Qed.
Lemma add_one (p: peirce):
AxiomList ⊢ ∀∀ σ ($0 ⊕ $1) === ($0 ⊕ $1) ⊕ σ zero.
Proof.
fstart. fintros "x" "y". fassert ((y ⊕ x) ⊕ σ zero === σ ((y ⊕ x) ⊕ zero)) as "->".
fapply add_rec_right.
fassert (y ⊕ x === (y ⊕ x) ⊕ zero) as "<-".
fapply x_plus_zero. fapply ((form_inclusion ax_refl)).
Qed.
Lemma σ_large_injective (p: peirce):
AxiomList ⊢ ∀∀∀ $2 === σ (($2 ⊕ $1) ⊕ $0) → ⊥.
Proof.
fstart. unfold AxiomList. unfold ax_induction'. fapply 3.
- fintros "k" "k'". fapply ((form_inclusion ax_zero_succ)).
- fintros "x" "IH" "k" "k'". fintros "H".
fapply ("IH" k k'). frewrite <- ((form_inclusion ax_add_rec) k' (x ⊕ k)).
frewrite <- ((form_inclusion ax_add_rec) k x).
fapply ((form_inclusion ax_succ_inj)). fapply "H".
Qed.
Lemma add_assoc (p: peirce):
AxiomList ⊢ ∀∀∀ ($0 ⊕ $1) ⊕ $2 === $0 ⊕ ($1 ⊕ $2).
Proof.
fstart. unfold AxiomList. unfold ax_induction'. fapply 4.
- fintros "y" "x". frewrite <- (x_plus_zero y).
frewrite <- (x_plus_zero (x ⊕ y)). fapply ((form_inclusion ax_refl)).
- fintros "z" "IH" "y" "x". frewrite (add_rec_right y z).
frewrite (add_rec_right (x ⊕ y) z). frewrite (add_rec_right x (y ⊕ z)).
fapply ((form_inclusion ax_succ_congr)). fapply "IH".
Qed.
Lemma ineq_sandwich (p: peirce):
AxiomList ⊢ ∀∀ $1 ⧀l $0 → $0 ⧀l σ $1 → ⊥.
Proof.
fstart. fintros "x" "y" "[k Hk]" "[k' Hk']".
fassert (x === σ (x ⊕ k) ⊕ k') as "Hx".
fapply ((form_inclusion ax_succ_inj)). frewrite <- ((form_inclusion ax_add_rec) k x).
frewrite <- "Hk". frewrite <- ((form_inclusion ax_add_rec) k' y). fapply "Hk'".
fapply (σ_large_injective x k k'). frewrite <- ((form_inclusion ax_add_rec) k' (x ⊕ k)).
fapply "Hx".
Qed.
Lemma less_by_one (p: peirce):
AxiomList ⊢ ∀∀ σ $0 === $1 → $0 ⧀l $1.
Proof.
fstart. fintros "a" "b" "Hab". fexists zero.
frewrite "Hab". fapply x_plus_zero.
Qed.
Lemma ineq_plus (p: peirce):
AxiomList ⊢ ∀∀∀ $0 ⧀l $1 → $2 ⊕ $0 ⧀l $2 ⊕ $1.
Proof.
fstart. fintros "k" "y" "x" "[k' Hk']". fexists k'. frewrite "Hk'".
frewrite ((form_inclusion ax_add_rec) k' (k ⊕ x)).
frewrite ((form_inclusion ax_add_rec) k' x). frewrite (add_rec_right k (x ⊕ k')).
fapply ((form_inclusion ax_succ_congr)). frewrite (add_assoc k' x k).
fapply ((form_inclusion ax_refl)).
Qed.
Lemma ineq_dec (p: peirce):
AxiomList ⊢ ∀∀ $0 ⧀l $1 ∨ $1 ⧀l $0 ∨ $1 === $0.
Proof.
fstart. unfold AxiomList. unfold ax_induction'. fapply 5.
- fintros "y". fassert (y === zero ∨ ∃ y`[↑] === σ $0) as "[Heq|[k Hk]]".
fapply ((form_inclusion ax_cases)).
+ fright. fapply ((form_inclusion ax_sym)). fapply "Heq".
+ fleft. fright. fexists k. frewrite ((form_inclusion ax_add_rec) k zero).
frewrite ((form_inclusion ax_add_zero) k). fapply "Hk".
- fintros "x" "IH" "y". fassert (y === zero ∨ ∃ y`[↑] === σ $0) as "[Heq|[y' Hy']]".
fapply ((form_inclusion ax_cases)).
+ fleft. fleft. fexists x. frewrite "Heq".
frewrite ((form_inclusion ax_add_rec) x zero).
frewrite ((form_inclusion ax_add_zero) x). fapply ((form_inclusion ax_refl)).
+ fdestruct ("IH" y') as "[[[k Hk]|[k Hk]]|Heq]".
* fleft. fleft. fexists k. frewrite "Hy'".
frewrite ((form_inclusion ax_add_rec) k (σ y')).
fapply ((form_inclusion ax_succ_congr)). fapply "Hk".
* fleft. fright. fexists k. frewrite "Hy'".
frewrite ((form_inclusion ax_add_rec) k (σ x)).
fapply ((form_inclusion ax_succ_congr)). fapply "Hk".
* fright. frewrite "Heq". frewrite "Hy'".
fapply ((form_inclusion ax_refl)).
Qed.
Lemma ineq_trans (p: peirce):
AxiomList ⊢ ∀∀∀ $0 ⧀l $1 → $1 ⧀l $2 → $0 ⧀l $2.
Proof.
fstart. fintros "z" "y" "x". fintros "[k Hk]" "[k' Hk']".
fexists (k ⊕ σ k'). fassert ((σ x ⊕ k) ⊕ σ k' === σ x ⊕ (k ⊕ σ k')) as "<-". fapply add_assoc. frewrite <- "Hk".
fassert (y ⊕ σ k' === σ (y ⊕ k')) as "->". fapply add_rec_right.
frewrite <- ((form_inclusion ax_add_rec) k' y). fapply "Hk'".
Qed.
Lemma len_app_plus_one (p: peirce):
AxiomList ⊢ ∀∀∀ σ (len $0 ⊕ len $1) === len (($0 +++ $1) +++ ($2 ::: [|])).
Proof.
fstart. fintros "t2" "y" "x".
fassert (∀∀ len ($0 +++ $1) === len $0 ⊕ len $1) as "Hax_len_app".
fintros "a" "b". fapply ax_len_app.
fassert (∀∀ len ($0 ::: $1) === σ (len $1)) as "Hax_len_cons".
fintros "a" "b". fapply ax_len_cons.
fassert (len [|] === zero) as "Hax_len_nil".
fapply ax_len_nil.
frewrite ("Hax_len_app" (t2 ::: [|]) (x +++ y)). frewrite ("Hax_len_app" y x).
frewrite ("Hax_len_cons" [|] t2). frewrite "Hax_len_nil". fapply add_one.
Qed.
Lemma len_app_ineq (p: peirce):
AxiomList ⊢ ∀∀∀ $0 ⧀l len $1 → $0 ⧀l len ($1 +++ $2).
Proof.
fstart. fintros "y" "x" "i" "[k Hk]".
fexists (k ⊕ len y). frewrite (ax_len_app y x).
fassert ((σ i ⊕ k) ⊕ len y === σ i ⊕ (k ⊕ len y)) as "<-". fapply add_assoc.
frewrite <- "Hk". fapply ((form_inclusion ax_refl)).
Qed.
Lemma len_app_ineq' (p: peirce):
AxiomList ⊢ ∀∀∀ $0 ⧀l len $2 → len $1 ⊕ $0 ⧀l len ($1 +++ $2).
Proof.
fstart. fintros "y" "x" "i" "[k Hk]". fexists k.
frewrite (ax_len_app y x). fassert (len x ⊕ σ i === σ (len x ⊕ i)) as "<-". fapply add_rec_right. frewrite (add_assoc k (σ i) (len x)).
frewrite <- "Hk". fapply ((form_inclusion ax_refl)).
Qed.
Lemma get_low_index' (p: peirce):
AxiomList ⊢ ∀∀∀∀ $0 ⧀l len $1 → ((($1 +++ $2) +++ $3) G $0) === ($1 G $0).
Proof.
fstart. fintros "z" "y" "x" "i". fintros "Hi".
fassert (((x +++ y) +++ z G i) === ((x +++ y) G i)) as "->".
fapply ax_get_app_left. fapply len_app_ineq. fapply "Hi".
fapply ax_get_app_left. fapply "Hi".
Qed.
Lemma get_low_index (p: peirce):
AxiomList ⊢ ∀∀∀∀∀ $0 ⧀l $1 → $1 ⧀l len $2 → ((($2 +++ $3) +++ $4) G $0) === ($2 G $0).
Proof.
fstart. fintros "z" "y" "x" "j". fintros "i" "Hj" "Hi".
fassert (i ⧀l len x) as "Hi'". feapply ineq_trans. feapply "Hj". fapply "Hi".
fapply get_low_index'. fapply "Hi'".
Qed.
Lemma get_mid_index' (p: peirce):
AxiomList ⊢ ∀∀∀∀ $0 ⧀l len $2 → ((($1 +++ $2) +++ $3) G (len $1 ⊕ $0)) === ($2 G $0).
Proof.
fstart. fintros "z" "y" "x" "i". fintros "Hi".
fassert (((x +++ y) +++ z G (len x ⊕ i)) === ((x +++ y) G (len x ⊕ i))) as "->".
fapply ax_get_app_left. fapply len_app_ineq'. fapply "Hi".
frewrite (add_comm i (len x)). fapply ax_get_app_right. fapply "Hi".
Qed.
Lemma get_mid_index (p: peirce):
AxiomList ⊢ ∀∀∀∀∀ $0 ⧀l $1 → $1 ⧀l len $3 → ((($2 +++ $3) +++ $4) G (len $2 ⊕ $0)) === ($3 G $0).
Proof.
fstart. fintros "t2" "y" "x" "j". fintros "i" "Hj" "Hi".
fassert (i ⧀l len y) as "Hi'". feapply ineq_trans. feapply "Hj". feapply "Hi".
fapply get_mid_index'. fapply "Hi'".
Qed.
Lemma add_cancel (p: peirce):
AxiomList ⊢ ∀∀∀ $2 ⊕ $0 === $2 ⊕ $1 → $0 === $1.
Proof.
fstart. unfold AxiomList. unfold ax_induction'. fapply 6.
- fintros "z" "y". frewrite ((form_inclusion ax_add_zero) y).
frewrite ((form_inclusion ax_add_zero) z). fintros "H"; fapply "H".
- fintros "x" "IH" "z" "y". frewrite ((form_inclusion ax_add_rec) y x).
frewrite ((form_inclusion ax_add_rec) z x). fintros "H". fapply "IH".
fapply ((form_inclusion ax_succ_inj)). fapply "H".
Qed.
Will be used for the following: len x ⧀l i → i ⧀ len x ⊕ len y → ∃ j ⧀ len y, i === len x ⊕ j
Lemma index_destruct' (p: peirce):
AxiomList ⊢ ∀∀∀ $1 ⧀=l $0 → $0 ⧀l $1 ⊕ $2 → ∃ $0 ⧀l $3 ∧ $1 === $2 ⊕ $0.
Proof.
fstart. fintros "y" "x" "j" "[l Hl]". fintros "[m Hm]".
fexists l. fsplit; last fapply "Hl".
fexists m. fapply (add_cancel x (σ l ⊕ m) y). frewrite "Hm".
frewrite "Hl". fassert ((x ⊕ σ l) === σ (x ⊕ l)) as "<-".
fapply add_rec_right. fapply add_assoc.
Qed.
Lemma index_destruct (p: peirce):
AxiomList ⊢ ∀∀∀ $1 ⧀l $0 ∨ $1 === $0 → $0 ⧀l $1 ⊕ $2 → ∃ $0 ⧀l $3 ∧ $1 === $2 ⊕ $0.
Proof.
fstart. fintros "y" "x" "j" "[[l Hl]|Heq]".
- fapply index_destruct'. fexists (σ l).
fassert (x ⊕ σ l === σ (x ⊕ l)) as "->". fapply add_rec_right.
frewrite <- ((form_inclusion ax_add_rec) l x). fapply "Hl".
- fapply index_destruct'. fexists zero. frewrite "Heq". fapply x_plus_zero.
Qed.
Lemma get_last_triple_app (p: peirce):
AxiomList ⊢ ∀∀∀ ((($0 +++ $1) +++ ($2 ::: [|]) G len $0 ⊕ len $1) === $2).
Proof.
fstart. fintros t2 y x.
fassert (∀∀ len ($0 +++ $1) === len $0 ⊕ len $1) as "Hax_len_app".
fintros "a" "b". fapply ax_len_app.
fassert (∀∀ len ($0 ::: $1) === σ (len $1)) as "Hax_len_cons".
fintros "a" "b". fapply ax_len_cons.
fassert (len [|] === zero) as "Hax_len_nil".
fapply ax_len_nil.
fassert (∀∀∀ $2 ⧀l len $1 → (($0 +++ $1) G ($2 ⊕ len $0)) === ($1 G $2)) as "Hax_get_app_right".
fintros "a" "b" "c". fapply ax_get_app_right.
fassert (∀ zero ⊕ $0 === $0) as "Hax_add_zero".
fintros "a". cbn. fapply ((∀ zero ⊕ $0 === $0)).
fassert (∀∀ ($0 ::: $1) G zero === $0) as "Hax_get_zero".
fintros "a" "b". fapply ax_get_zero.
fassert (zero ⧀l len (t2 ::: [|])) as "Hlen".
fexists (zero). frewrite (ax_len_cons [|] t2). frewrite "Hax_len_nil".
fapply (x_plus_zero). fspecialize ("Hax_get_app_right" zero (t2 ::: [|]) (x +++ y)).
fspecialize ("Hax_get_app_right" "Hlen"). frewrite <- ("Hax_add_zero" (len x ⊕ len y)).
frewrite <- ("Hax_len_app" y x). frewrite "Hax_get_app_right".
frewrite ("Hax_get_zero" [|] t2). fapply ((∀ $0 === $0)).
Qed.
AxiomList ⊢ ∀∀∀ $1 ⧀=l $0 → $0 ⧀l $1 ⊕ $2 → ∃ $0 ⧀l $3 ∧ $1 === $2 ⊕ $0.
Proof.
fstart. fintros "y" "x" "j" "[l Hl]". fintros "[m Hm]".
fexists l. fsplit; last fapply "Hl".
fexists m. fapply (add_cancel x (σ l ⊕ m) y). frewrite "Hm".
frewrite "Hl". fassert ((x ⊕ σ l) === σ (x ⊕ l)) as "<-".
fapply add_rec_right. fapply add_assoc.
Qed.
Lemma index_destruct (p: peirce):
AxiomList ⊢ ∀∀∀ $1 ⧀l $0 ∨ $1 === $0 → $0 ⧀l $1 ⊕ $2 → ∃ $0 ⧀l $3 ∧ $1 === $2 ⊕ $0.
Proof.
fstart. fintros "y" "x" "j" "[[l Hl]|Heq]".
- fapply index_destruct'. fexists (σ l).
fassert (x ⊕ σ l === σ (x ⊕ l)) as "->". fapply add_rec_right.
frewrite <- ((form_inclusion ax_add_rec) l x). fapply "Hl".
- fapply index_destruct'. fexists zero. frewrite "Heq". fapply x_plus_zero.
Qed.
Lemma get_last_triple_app (p: peirce):
AxiomList ⊢ ∀∀∀ ((($0 +++ $1) +++ ($2 ::: [|]) G len $0 ⊕ len $1) === $2).
Proof.
fstart. fintros t2 y x.
fassert (∀∀ len ($0 +++ $1) === len $0 ⊕ len $1) as "Hax_len_app".
fintros "a" "b". fapply ax_len_app.
fassert (∀∀ len ($0 ::: $1) === σ (len $1)) as "Hax_len_cons".
fintros "a" "b". fapply ax_len_cons.
fassert (len [|] === zero) as "Hax_len_nil".
fapply ax_len_nil.
fassert (∀∀∀ $2 ⧀l len $1 → (($0 +++ $1) G ($2 ⊕ len $0)) === ($1 G $2)) as "Hax_get_app_right".
fintros "a" "b" "c". fapply ax_get_app_right.
fassert (∀ zero ⊕ $0 === $0) as "Hax_add_zero".
fintros "a". cbn. fapply ((∀ zero ⊕ $0 === $0)).
fassert (∀∀ ($0 ::: $1) G zero === $0) as "Hax_get_zero".
fintros "a" "b". fapply ax_get_zero.
fassert (zero ⧀l len (t2 ::: [|])) as "Hlen".
fexists (zero). frewrite (ax_len_cons [|] t2). frewrite "Hax_len_nil".
fapply (x_plus_zero). fspecialize ("Hax_get_app_right" zero (t2 ::: [|]) (x +++ y)).
fspecialize ("Hax_get_app_right" "Hlen"). frewrite <- ("Hax_add_zero" (len x ⊕ len y)).
frewrite <- ("Hax_len_app" y x). frewrite "Hax_get_app_right".
frewrite ("Hax_get_zero" [|] t2). fapply ((∀ $0 === $0)).
Qed.
Lemma modus_ponens_step (p: peirce):
AxiomList ⊢ ∀∀∀∀∀∀∀ σ $2 === len $0 → σ $3 === len $1 →
($0 G $2) === $4 → ($1 G $3) === ($4 ~> $5) → $6 === len $0 ⊕ len $1 →
well_formed[$6 .: (($0 +++ $1) +++ ($5 ::: [|]))..].
Proof.
fstart. fintros "i" "t2" "t1" "s2". fintros "s1" "y" "x". fintros "Hs1" "Hs2" "Hx" "Hy". fintros "Hsum".
fassert (∀∀ len ($0 +++ $1) === len $0 ⊕ len $1) as "Hax_len_app".
fintros "a" "b". fapply ax_len_app.
fassert (∀∀ len ($0 ::: $1) === σ (len $1)) as "Hax_len_cons".
fintros "a" "b". fapply ax_len_cons.
fassert (∀∀∀ $2 ⧀l len $1 → (($0 +++ $1) G ($2 ⊕ len $0)) === ($1 G $2)) as "Hax_get_app_right".
fintros "a" "b" "c". fapply ax_get_app_right.
fassert (∀∀∀ $2 ⧀l len $0 → (($0 +++ $1) G $2) === ($0 G $2)) as "Hax_get_app_left".
fintros "a" "b" "c". fapply ax_get_app_left.
fassert (∀ zero ⊕ $0 === $0) as "Hax_add_zero".
fintros "a". cbn. fapply ((∀ zero ⊕ $0 === $0)).
fassert (∀ (∀ σ $0 ⊕ $1 === σ ($0 ⊕ $1))) as "Hax_add_rec".
fintros "a" "b". fapply ((∀ (∀ σ $0 ⊕ $1 === σ ($0 ⊕ $1)))).
fassert (∀∀ ($0 ::: $1) G zero === $0) as "Hax_get_zero".
fintros "a" "b". fapply ax_get_zero.
fassert (∀ $0 === $0 ⊕ zero) as "x_plus_zero".
fintros "a". fapply x_plus_zero.
fassert (len [|] === zero) as "Hax_len_nil".
fapply ax_len_nil.
fright. fexists s1. fexists (s2 ⊕ len x). repeat fsplit.
- fexists zero. frewrite <- ("x_plus_zero" (σ (s2 ⊕ len x))). frewrite <- ("Hax_add_rec" (len x) s2).
frewrite "Hs2". frewrite "Hsum". fapply add_comm.
- fexists (len y). frewrite "Hs1". fapply "Hsum".
- pose (l := (x +++ y) +++ (t2 ::: [|])). fold l.
fassert ((l G (s2 ⊕ len x)) === ((x +++ y) G (s2 ⊕ len x))) as "->".
fapply "Hax_get_app_left". fapply (less_by_one (len (x +++ y)) (s2 ⊕ len x)).
frewrite <- ("Hax_add_rec" (len x) s2). frewrite "Hs2".
frewrite ("Hax_len_app" y x). fapply add_comm.
fassert (((x +++ y) G (s2 ⊕ len x)) === (y G s2)) as "->".
fapply "Hax_get_app_right". fexists zero. frewrite <- ("x_plus_zero" (σ s2)).
frewrite "Hs2". fapply ((∀ $0 === $0)). fold l.
fassert ((l G s1) === ((x +++ y) G s1)) as "->". fapply ax_get_app_left.
fexists (len y). frewrite "Hs1". fapply ax_len_app.
fassert (((x +++ y) G s1) === (x G s1)) as "->". fapply ax_get_app_left.
fapply (less_by_one (len x) s1). fapply "Hs1". fold l.
fassert ((l G i) === ((t2 ::: [|]) G zero)) as "->".
fassert (i === (len (x +++ y)) ⊕ zero) as "->". frewrite <- ("x_plus_zero" (len (x +++ y))).
frewrite ("Hax_len_app" y x). fapply "Hsum".
frewrite (add_comm zero (len (x +++ y))). fapply ax_get_app_right.
fapply (less_by_one (len (t2 ::: [|])) zero). frewrite ("Hax_len_cons" [|] t2).
frewrite "Hax_len_nil". fapply ((∀ $0 === $0)).
frewrite ("Hax_get_zero" [|] t2). frewrite "Hx".
frewrite "Hy". fapply ((∀ $0 === $0)).
Qed.
Ltac ax_subst_simpl := rewrite !subst_comp; eapply bounded_subst; eauto;
intros []; try lia; cbn; asimpl; easy.
Lemma well_formed_propagation (p: peirce):
AxiomList ⊢ ∀∀∀∀ $0 ⧀l len $1 ⊕ len $2 → (∀ $0 ⧀l len $2 → well_formed[$0 .: $2..])
→ (∀ $0 ⧀l len $3 → well_formed[$0 .: $3..]) → well_formed[$0 .: (($2 +++ $1) +++ ($3 ::: [|]))..].
Proof.
fstart. fintros "t2" "x" "y" "i". fintros "[k Hk]" "Himpl" "Hpre".
fassert (∀∀ $0 ⧀l $1 ∨ $1 ⧀l $0 ∨ $1 === $0) as "ineq_dec".
fintros "a" "b". fapply ineq_dec.
fassert (∀∀ $0 ⧀l $1 ∨ ($1 ⧀l $0 ∨ $1 === $0)) as "ineq_dec'".
fintros "a" "b". fdestruct ("ineq_dec" a b) as "[[H|H]|H]". fleft. fapply "H". fright. fleft. fapply "H". fright. fright. fapply "H".
fassert (∀∀∀ $1 ⧀l $0 ∨ $1 === $0 → $0 ⧀l $1 ⊕ $2 → ∃ $0 ⧀l $3 ∧ $1 === $2 ⊕ $0) as "index_destruct".
fintros "a" "b" "c". fapply index_destruct.
fassert (∀∀∀ $0 ⧀l $1 → $2 ⊕ $0 ⧀l $2 ⊕ $1) as "ineq_plus".
fintros "a" "b" "c". fapply ineq_plus.
replace (ax[_][_][_][_][_][i..]) with (ax[(((x +++ y) +++ (t2 ::: [|])) G i)..]).
2: { ax_subst_simpl. }
fassert (((x +++ y) +++ (t2 ::: [|]) G i) === ((x +++ y) G i)) as "Hgeti".
fapply ax_get_app_left. fexists k. frewrite (ax_len_app y x). frewrite <- "Hk". fapply add_comm.
fdestruct ("ineq_dec'" (len x) i) as "[Hix|Hix]".
- fspecialize ("Hpre" i). fdestruct ("Hpre" "Hix") as "[Hax|[j [j' [[Hj' Hj] Hjj'impl]]]]". + fleft. replace (ax[_][_][_][_][_][_][_]) with (ax[(x G i)..]).
2: { ax_subst_simpl. }
fassert (((x +++ y) G i) === (x G i)) as "Hgeti'".
fapply ax_get_app_left. fapply "Hix". feapply QEqLi_leibniz; last fapply "Hax".
frewrite <- "Hgeti'". frewrite "Hgeti". fapply ((∀ $0 === $0)).
+ fright. fexists j. fexists j'. repeat fsplit.
* fapply "Hj'".
* fapply "Hj".
* fassert (((x +++ y) +++ (t2 ::: [|]) G j') === (x G j')) as "->". feapply get_low_index.
fapply "Hj'". fapply "Hix".
fassert (((x +++ y) +++ (t2 ::: [|]) G j) === (x G j)) as "->". feapply get_low_index.
fapply "Hj". fapply "Hix".
fassert (((x +++ y) +++ (t2 ::: [|]) G i) === (x G i)) as "->". feapply get_low_index'.
fapply "Hix". fapply "Hjj'impl".
- fspecialize ("index_destruct" (len y) (len x) i).
fassert (i ⧀l (len x) ⊕ (len y)) as "Hi'". fexists k. frewrite <- "Hk". fapply add_comm.
fdestruct ("index_destruct" "Hix" "Hi'") as "[a [Haleq Haeq]]".
fspecialize ("Himpl" a). fdestruct ("Himpl" "Haleq") as "[Hax|[j [j' [[Hj' Hj] Hjj'impl]]]]".
+ fleft. replace (ax[_][_][_][_][_][_][_]) with (ax[(y G a)..]).
2: { ax_subst_simpl. }
feapply QEqLi_leibniz; last fapply "Hax".
fapply ((∀ (∀ $1 === $0 → $0 === $1))). frewrite "Haeq". fapply get_mid_index'.
fapply "Haleq".
+ fright. fexists (len x ⊕ j). fexists (len x ⊕ j'). repeat fsplit.
* frewrite "Haeq". fspecialize ("ineq_plus" (len x) a j').
fspecialize ("ineq_plus" "Hj'"). fapply "ineq_plus".
* frewrite "Haeq". fspecialize ("ineq_plus" (len x) a j).
fspecialize ("ineq_plus" "Hj"). fapply "ineq_plus".
* fassert (((x +++ y) +++ (t2 ::: [|]) G len x ⊕ j') === (y G j')) as "->". feapply get_mid_index.
feapply "Hj'". fapply "Haleq".
fassert (((x +++ y) +++ (t2 ::: [|]) G len x ⊕ j) === (y G j)) as "->". feapply get_mid_index.
feapply "Hj". fapply "Haleq".
fassert (((x +++ y) +++ (t2 ::: [|]) G i) === (y G a)) as "->".
frewrite "Haeq". fapply get_mid_index'. fapply "Haleq".
fapply "Hjj'impl".
Qed.
Global Opaque well_formed.
Ltac well_formed_subst_simpl n := rewrite !subst_comp; eapply bounded_subst; first apply well_formed_bound; intros[]; try lia; cbn; first easy;
intros Hn; assert (n = 0) as -> by lia; cbn; asimpl; easy.
Lemma box_distr (t1 t2: term) (p: peirce):
bounded_t 0 t1 -> bounded_t 0 t2 -> AxiomList ⊢ prov[t1..] → prov[(t1 ~> t2)..] → prov[t2..].
Proof.
intros Ht1 Ht2. fstart.
fassert (∀∀ len ($0 +++ $1) === len $0 ⊕ len $1) as "Hax_len_app".
fintros "a" "b". fapply ax_len_app.
fassert (∀∀ len ($0 ::: $1) === σ (len $1)) as "Hax_len_cons".
fintros "a" "b". fapply ax_len_cons.
fassert (len [|] === zero) as "Hax_len_nil".
fapply ax_len_nil.
fassert (∀∀ $0 ⧀l $1 ∨ $1 ⧀l $0 ∨ $1 === $0) as "ineq_dec".
fintros "a" "b". fapply ineq_dec.
fassert (∀∀∀∀ $0 ⧀l len $1 ⊕ len $2 → (∀ $0 ⧀l len $2 → well_formed[$0 .: $2..])
→ (∀ $0 ⧀l len $3 → well_formed[$0 .: $3..]) → well_formed[$0 .: (($2 +++ $1) +++ ($3 ::: [|]))..]) as "propagation".
fintros "a" "b" "c" "d". fapply well_formed_propagation.
fassert (∀∀∀∀∀∀∀ σ $2 === len $0 → σ $3 === len $1 →
($0 G $2) === $4 → ($1 G $3) === ($4 ~> $5) → $6 === len $0 ⊕ len $1 →
well_formed[$6 .: (($0 +++ $1) +++ ($5 ::: [|]))..]) as "modus_ponens_step".
fintros "a" "b" "c" "d". fintros "e" "f" "g". fapply modus_ponens_step.
fintros "[x [[s1 [Hlen1 Hlast1]] Hpre]]". fintros "[y [[s2 [Hlen2 Hlast2]] Himpl]]".
repeat rewrite (bounded_t_0_subst ↑ Ht1). repeat rewrite (bounded_t_0_subst ↑ Ht2).
fexists ((x +++ y) +++ (t2 ::: [|])).
fsplit.
- fexists (len x ⊕ len y). repeat rewrite (bounded_t_0_subst _ Ht2). fsplit; first fapply len_app_plus_one.
fapply get_last_triple_app.
- fintros "i" "Hi".
fassert (len (x +++ y) === len x ⊕ len y) as "Hlenxy". fapply ax_len_app.
fassert (len ((x +++ y) +++ (t2 ::: [|])) === (len x ⊕ len y) ⊕ σ zero) as "HlenTot".
frewrite ("Hax_len_app" (t2:::[|]) (x+++y)). frewrite "Hlenxy".
frewrite ("Hax_len_cons" [|] t2). frewrite "Hax_len_nil". fapply ((∀ $0 === $0)).
fdestruct ("ineq_dec" i (len y ⊕ len x)) as "[[[k Hk]|HiLe]|HiEq]".
+ fexfalso. fapply (ineq_sandwich (len x ⊕ len y) i).
* fexists k. frewrite (add_comm (len y) (len x)). fapply "Hk".
* fdestruct "Hi" as "[k' Hk']". fexists k'. frewrite (add_one (len y) (len x)).
frewrite <- "HlenTot". fapply "Hk'".
+ fspecialize ("propagation" t2 x y). fspecialize ("propagation" i).
replace (well_formed[$0 .: _..][up (up (up (up t2..)))][up (up (up x..))][up (up y..)][up i..]) with (well_formed[$0 .: y`[↑]..]).
2: { well_formed_subst_simpl n. }
replace (well_formed[$0 .: _][up (_ .: $0 ..)][up (up (t1 ~> t2)..)][up y..]) with (well_formed[$0 .: y`[↑]..]).
2: { well_formed_subst_simpl n. }
replace (well_formed[ $0 .: _ ..][up ( _ .: $0..)][_][_]) with (well_formed[$0 .: (x`[↑])..]).
2: { well_formed_subst_simpl n. }
replace (well_formed[$0 .: _..][_][_][_][_]) with (well_formed[$0 .: (x`[↑])..]).
2: { well_formed_subst_simpl n. }
fspecialize ("propagation" "HiLe" "Himpl" "Hpre").
replace (well_formed[_][up (up (up t2..))][_][_][i..]) with
(well_formed[$0 .: $2..][up ($1 .: $0..)][up (up t2..)][up ((x +++ y) +++ (t2 ::: [|]))..][i..]).
2: { well_formed_subst_simpl n. }
fapply "propagation".
+ fspecialize ("modus_ponens_step" i t2 t1). fspecialize ("modus_ponens_step" s2 s1 y).
fspecialize ("modus_ponens_step" x). fspecialize ("modus_ponens_step" "Hlen1" "Hlen2" "Hlast1").
fspecialize ("modus_ponens_step" "Hlast2").
replace (well_formed[_][_][_][_][_][_][_][_])
with (well_formed[$0 .: $2..][up ($1 .: $0..)][up (up t2..)][up ((x +++ y) +++ (t2 ::: [|]))..][i..]).
2: { rewrite !subst_comp; eapply bounded_subst; first apply well_formed_bound. intros[]; try lia; cbn.
- intros _. asimpl. easy.
- intros Hn. assert (n = 0) as -> by lia. cbn. asimpl. easy. }
fapply "modus_ponens_step". frewrite "HiEq". fapply add_comm.
Qed.
End DefProv.
AxiomList ⊢ ∀∀∀∀∀∀∀ σ $2 === len $0 → σ $3 === len $1 →
($0 G $2) === $4 → ($1 G $3) === ($4 ~> $5) → $6 === len $0 ⊕ len $1 →
well_formed[$6 .: (($0 +++ $1) +++ ($5 ::: [|]))..].
Proof.
fstart. fintros "i" "t2" "t1" "s2". fintros "s1" "y" "x". fintros "Hs1" "Hs2" "Hx" "Hy". fintros "Hsum".
fassert (∀∀ len ($0 +++ $1) === len $0 ⊕ len $1) as "Hax_len_app".
fintros "a" "b". fapply ax_len_app.
fassert (∀∀ len ($0 ::: $1) === σ (len $1)) as "Hax_len_cons".
fintros "a" "b". fapply ax_len_cons.
fassert (∀∀∀ $2 ⧀l len $1 → (($0 +++ $1) G ($2 ⊕ len $0)) === ($1 G $2)) as "Hax_get_app_right".
fintros "a" "b" "c". fapply ax_get_app_right.
fassert (∀∀∀ $2 ⧀l len $0 → (($0 +++ $1) G $2) === ($0 G $2)) as "Hax_get_app_left".
fintros "a" "b" "c". fapply ax_get_app_left.
fassert (∀ zero ⊕ $0 === $0) as "Hax_add_zero".
fintros "a". cbn. fapply ((∀ zero ⊕ $0 === $0)).
fassert (∀ (∀ σ $0 ⊕ $1 === σ ($0 ⊕ $1))) as "Hax_add_rec".
fintros "a" "b". fapply ((∀ (∀ σ $0 ⊕ $1 === σ ($0 ⊕ $1)))).
fassert (∀∀ ($0 ::: $1) G zero === $0) as "Hax_get_zero".
fintros "a" "b". fapply ax_get_zero.
fassert (∀ $0 === $0 ⊕ zero) as "x_plus_zero".
fintros "a". fapply x_plus_zero.
fassert (len [|] === zero) as "Hax_len_nil".
fapply ax_len_nil.
fright. fexists s1. fexists (s2 ⊕ len x). repeat fsplit.
- fexists zero. frewrite <- ("x_plus_zero" (σ (s2 ⊕ len x))). frewrite <- ("Hax_add_rec" (len x) s2).
frewrite "Hs2". frewrite "Hsum". fapply add_comm.
- fexists (len y). frewrite "Hs1". fapply "Hsum".
- pose (l := (x +++ y) +++ (t2 ::: [|])). fold l.
fassert ((l G (s2 ⊕ len x)) === ((x +++ y) G (s2 ⊕ len x))) as "->".
fapply "Hax_get_app_left". fapply (less_by_one (len (x +++ y)) (s2 ⊕ len x)).
frewrite <- ("Hax_add_rec" (len x) s2). frewrite "Hs2".
frewrite ("Hax_len_app" y x). fapply add_comm.
fassert (((x +++ y) G (s2 ⊕ len x)) === (y G s2)) as "->".
fapply "Hax_get_app_right". fexists zero. frewrite <- ("x_plus_zero" (σ s2)).
frewrite "Hs2". fapply ((∀ $0 === $0)). fold l.
fassert ((l G s1) === ((x +++ y) G s1)) as "->". fapply ax_get_app_left.
fexists (len y). frewrite "Hs1". fapply ax_len_app.
fassert (((x +++ y) G s1) === (x G s1)) as "->". fapply ax_get_app_left.
fapply (less_by_one (len x) s1). fapply "Hs1". fold l.
fassert ((l G i) === ((t2 ::: [|]) G zero)) as "->".
fassert (i === (len (x +++ y)) ⊕ zero) as "->". frewrite <- ("x_plus_zero" (len (x +++ y))).
frewrite ("Hax_len_app" y x). fapply "Hsum".
frewrite (add_comm zero (len (x +++ y))). fapply ax_get_app_right.
fapply (less_by_one (len (t2 ::: [|])) zero). frewrite ("Hax_len_cons" [|] t2).
frewrite "Hax_len_nil". fapply ((∀ $0 === $0)).
frewrite ("Hax_get_zero" [|] t2). frewrite "Hx".
frewrite "Hy". fapply ((∀ $0 === $0)).
Qed.
Ltac ax_subst_simpl := rewrite !subst_comp; eapply bounded_subst; eauto;
intros []; try lia; cbn; asimpl; easy.
Lemma well_formed_propagation (p: peirce):
AxiomList ⊢ ∀∀∀∀ $0 ⧀l len $1 ⊕ len $2 → (∀ $0 ⧀l len $2 → well_formed[$0 .: $2..])
→ (∀ $0 ⧀l len $3 → well_formed[$0 .: $3..]) → well_formed[$0 .: (($2 +++ $1) +++ ($3 ::: [|]))..].
Proof.
fstart. fintros "t2" "x" "y" "i". fintros "[k Hk]" "Himpl" "Hpre".
fassert (∀∀ $0 ⧀l $1 ∨ $1 ⧀l $0 ∨ $1 === $0) as "ineq_dec".
fintros "a" "b". fapply ineq_dec.
fassert (∀∀ $0 ⧀l $1 ∨ ($1 ⧀l $0 ∨ $1 === $0)) as "ineq_dec'".
fintros "a" "b". fdestruct ("ineq_dec" a b) as "[[H|H]|H]". fleft. fapply "H". fright. fleft. fapply "H". fright. fright. fapply "H".
fassert (∀∀∀ $1 ⧀l $0 ∨ $1 === $0 → $0 ⧀l $1 ⊕ $2 → ∃ $0 ⧀l $3 ∧ $1 === $2 ⊕ $0) as "index_destruct".
fintros "a" "b" "c". fapply index_destruct.
fassert (∀∀∀ $0 ⧀l $1 → $2 ⊕ $0 ⧀l $2 ⊕ $1) as "ineq_plus".
fintros "a" "b" "c". fapply ineq_plus.
replace (ax[_][_][_][_][_][i..]) with (ax[(((x +++ y) +++ (t2 ::: [|])) G i)..]).
2: { ax_subst_simpl. }
fassert (((x +++ y) +++ (t2 ::: [|]) G i) === ((x +++ y) G i)) as "Hgeti".
fapply ax_get_app_left. fexists k. frewrite (ax_len_app y x). frewrite <- "Hk". fapply add_comm.
fdestruct ("ineq_dec'" (len x) i) as "[Hix|Hix]".
- fspecialize ("Hpre" i). fdestruct ("Hpre" "Hix") as "[Hax|[j [j' [[Hj' Hj] Hjj'impl]]]]". + fleft. replace (ax[_][_][_][_][_][_][_]) with (ax[(x G i)..]).
2: { ax_subst_simpl. }
fassert (((x +++ y) G i) === (x G i)) as "Hgeti'".
fapply ax_get_app_left. fapply "Hix". feapply QEqLi_leibniz; last fapply "Hax".
frewrite <- "Hgeti'". frewrite "Hgeti". fapply ((∀ $0 === $0)).
+ fright. fexists j. fexists j'. repeat fsplit.
* fapply "Hj'".
* fapply "Hj".
* fassert (((x +++ y) +++ (t2 ::: [|]) G j') === (x G j')) as "->". feapply get_low_index.
fapply "Hj'". fapply "Hix".
fassert (((x +++ y) +++ (t2 ::: [|]) G j) === (x G j)) as "->". feapply get_low_index.
fapply "Hj". fapply "Hix".
fassert (((x +++ y) +++ (t2 ::: [|]) G i) === (x G i)) as "->". feapply get_low_index'.
fapply "Hix". fapply "Hjj'impl".
- fspecialize ("index_destruct" (len y) (len x) i).
fassert (i ⧀l (len x) ⊕ (len y)) as "Hi'". fexists k. frewrite <- "Hk". fapply add_comm.
fdestruct ("index_destruct" "Hix" "Hi'") as "[a [Haleq Haeq]]".
fspecialize ("Himpl" a). fdestruct ("Himpl" "Haleq") as "[Hax|[j [j' [[Hj' Hj] Hjj'impl]]]]".
+ fleft. replace (ax[_][_][_][_][_][_][_]) with (ax[(y G a)..]).
2: { ax_subst_simpl. }
feapply QEqLi_leibniz; last fapply "Hax".
fapply ((∀ (∀ $1 === $0 → $0 === $1))). frewrite "Haeq". fapply get_mid_index'.
fapply "Haleq".
+ fright. fexists (len x ⊕ j). fexists (len x ⊕ j'). repeat fsplit.
* frewrite "Haeq". fspecialize ("ineq_plus" (len x) a j').
fspecialize ("ineq_plus" "Hj'"). fapply "ineq_plus".
* frewrite "Haeq". fspecialize ("ineq_plus" (len x) a j).
fspecialize ("ineq_plus" "Hj"). fapply "ineq_plus".
* fassert (((x +++ y) +++ (t2 ::: [|]) G len x ⊕ j') === (y G j')) as "->". feapply get_mid_index.
feapply "Hj'". fapply "Haleq".
fassert (((x +++ y) +++ (t2 ::: [|]) G len x ⊕ j) === (y G j)) as "->". feapply get_mid_index.
feapply "Hj". fapply "Haleq".
fassert (((x +++ y) +++ (t2 ::: [|]) G i) === (y G a)) as "->".
frewrite "Haeq". fapply get_mid_index'. fapply "Haleq".
fapply "Hjj'impl".
Qed.
Global Opaque well_formed.
Ltac well_formed_subst_simpl n := rewrite !subst_comp; eapply bounded_subst; first apply well_formed_bound; intros[]; try lia; cbn; first easy;
intros Hn; assert (n = 0) as -> by lia; cbn; asimpl; easy.
Lemma box_distr (t1 t2: term) (p: peirce):
bounded_t 0 t1 -> bounded_t 0 t2 -> AxiomList ⊢ prov[t1..] → prov[(t1 ~> t2)..] → prov[t2..].
Proof.
intros Ht1 Ht2. fstart.
fassert (∀∀ len ($0 +++ $1) === len $0 ⊕ len $1) as "Hax_len_app".
fintros "a" "b". fapply ax_len_app.
fassert (∀∀ len ($0 ::: $1) === σ (len $1)) as "Hax_len_cons".
fintros "a" "b". fapply ax_len_cons.
fassert (len [|] === zero) as "Hax_len_nil".
fapply ax_len_nil.
fassert (∀∀ $0 ⧀l $1 ∨ $1 ⧀l $0 ∨ $1 === $0) as "ineq_dec".
fintros "a" "b". fapply ineq_dec.
fassert (∀∀∀∀ $0 ⧀l len $1 ⊕ len $2 → (∀ $0 ⧀l len $2 → well_formed[$0 .: $2..])
→ (∀ $0 ⧀l len $3 → well_formed[$0 .: $3..]) → well_formed[$0 .: (($2 +++ $1) +++ ($3 ::: [|]))..]) as "propagation".
fintros "a" "b" "c" "d". fapply well_formed_propagation.
fassert (∀∀∀∀∀∀∀ σ $2 === len $0 → σ $3 === len $1 →
($0 G $2) === $4 → ($1 G $3) === ($4 ~> $5) → $6 === len $0 ⊕ len $1 →
well_formed[$6 .: (($0 +++ $1) +++ ($5 ::: [|]))..]) as "modus_ponens_step".
fintros "a" "b" "c" "d". fintros "e" "f" "g". fapply modus_ponens_step.
fintros "[x [[s1 [Hlen1 Hlast1]] Hpre]]". fintros "[y [[s2 [Hlen2 Hlast2]] Himpl]]".
repeat rewrite (bounded_t_0_subst ↑ Ht1). repeat rewrite (bounded_t_0_subst ↑ Ht2).
fexists ((x +++ y) +++ (t2 ::: [|])).
fsplit.
- fexists (len x ⊕ len y). repeat rewrite (bounded_t_0_subst _ Ht2). fsplit; first fapply len_app_plus_one.
fapply get_last_triple_app.
- fintros "i" "Hi".
fassert (len (x +++ y) === len x ⊕ len y) as "Hlenxy". fapply ax_len_app.
fassert (len ((x +++ y) +++ (t2 ::: [|])) === (len x ⊕ len y) ⊕ σ zero) as "HlenTot".
frewrite ("Hax_len_app" (t2:::[|]) (x+++y)). frewrite "Hlenxy".
frewrite ("Hax_len_cons" [|] t2). frewrite "Hax_len_nil". fapply ((∀ $0 === $0)).
fdestruct ("ineq_dec" i (len y ⊕ len x)) as "[[[k Hk]|HiLe]|HiEq]".
+ fexfalso. fapply (ineq_sandwich (len x ⊕ len y) i).
* fexists k. frewrite (add_comm (len y) (len x)). fapply "Hk".
* fdestruct "Hi" as "[k' Hk']". fexists k'. frewrite (add_one (len y) (len x)).
frewrite <- "HlenTot". fapply "Hk'".
+ fspecialize ("propagation" t2 x y). fspecialize ("propagation" i).
replace (well_formed[$0 .: _..][up (up (up (up t2..)))][up (up (up x..))][up (up y..)][up i..]) with (well_formed[$0 .: y`[↑]..]).
2: { well_formed_subst_simpl n. }
replace (well_formed[$0 .: _][up (_ .: $0 ..)][up (up (t1 ~> t2)..)][up y..]) with (well_formed[$0 .: y`[↑]..]).
2: { well_formed_subst_simpl n. }
replace (well_formed[ $0 .: _ ..][up ( _ .: $0..)][_][_]) with (well_formed[$0 .: (x`[↑])..]).
2: { well_formed_subst_simpl n. }
replace (well_formed[$0 .: _..][_][_][_][_]) with (well_formed[$0 .: (x`[↑])..]).
2: { well_formed_subst_simpl n. }
fspecialize ("propagation" "HiLe" "Himpl" "Hpre").
replace (well_formed[_][up (up (up t2..))][_][_][i..]) with
(well_formed[$0 .: $2..][up ($1 .: $0..)][up (up t2..)][up ((x +++ y) +++ (t2 ::: [|]))..][i..]).
2: { well_formed_subst_simpl n. }
fapply "propagation".
+ fspecialize ("modus_ponens_step" i t2 t1). fspecialize ("modus_ponens_step" s2 s1 y).
fspecialize ("modus_ponens_step" x). fspecialize ("modus_ponens_step" "Hlen1" "Hlen2" "Hlast1").
fspecialize ("modus_ponens_step" "Hlast2").
replace (well_formed[_][_][_][_][_][_][_][_])
with (well_formed[$0 .: $2..][up ($1 .: $0..)][up (up t2..)][up ((x +++ y) +++ (t2 ::: [|]))..][i..]).
2: { rewrite !subst_comp; eapply bounded_subst; first apply well_formed_bound. intros[]; try lia; cbn.
- intros _. asimpl. easy.
- intros Hn. assert (n = 0) as -> by lia. cbn. asimpl. easy. }
fapply "modus_ponens_step". frewrite "HiEq". fapply add_comm.
Qed.
End DefProv.