(** * The Theory of Peano Arithmetic and its Coq model *) (** The NatDed development, Pierre Letouzey, 2019. This file is released under the CC0 License, see the LICENSE file *) Require Import Defs NameProofs Mix Meta Theories PreModels Models. Import ListNotations. Local Open Scope bool_scope. Local Open Scope eqb_scope. (** The Peano axioms *) Definition PeanoSign := Finite.to_infinite peano_sign. Definition Zero := Fun "O" []. Definition Succ x := Fun "S" [x]. Notation "x = y" := (Pred "=" [x;y]) : formula_scope. Notation "x + y" := (Fun "+" [x;y]) : formula_scope. Notation "x * y" := (Fun "*" [x;y]) : formula_scope. Module PeanoAx. Local Open Scope formula_scope. Definition ax1 := ∀ (#0 = #0). Definition ax2 := ∀∀ (#1 = #0 -> #0 = #1). Definition ax3 := ∀∀∀ (#2 = #1 /\ #1 = #0 -> #2 = #0). Definition ax4 := ∀∀ (#1 = #0 -> Succ (#1) = Succ (#0)). Definition ax5 := ∀∀∀ (#2 = #1 -> #2 + #0 = #1 + #0). Definition ax6 := ∀∀∀ (#1 = #0 -> #2 + #1 = #2 + #0). Definition ax7 := ∀∀∀ (#2 = #1 -> #2 * #0 = #1 * #0). Definition ax8 := ∀∀∀ (#1 = #0 -> #2 * #1 = #2 * #0). Definition ax9 := ∀ (Zero + #0 = #0). Definition ax10 := ∀∀ (Succ(#1) + #0 = Succ(#1 + #0)). Definition ax11 := ∀ (Zero * #0 = Zero). Definition ax12 := ∀∀ (Succ(#1) * #0 = (#1 * #0) + #0). Definition ax13 := ∀∀ (Succ(#1) = Succ(#0) -> #1 = #0). Definition ax14 := ∀ ~(Succ(#0) = Zero). Definition axioms_list := [ ax1; ax2; ax3; ax4; ax5; ax6; ax7; ax8; ax9; ax10; ax11; ax12; ax13; ax14 ]. (** Beware, [bsubst] is ok below for turning [#0] into [Succ #0], but only since it contains now a [lift] of substituted terms inside quantifiers. And the unconventional [∀] before [A[0]] is to get the right bounded vars (Hack !). *) Definition induction_schema A_x := let A_0 := bsubst 0 Zero A_x in let A_Sx := bsubst 0 (Succ(#0)) A_x in nForall (Nat.pred (level A_x)) (((∀ A_0) /\ (∀ (A_x -> A_Sx))) -> ∀ A_x). Local Close Scope formula_scope. Definition IsAx A := List.In A axioms_list \/ exists B, A = induction_schema B /\ check PeanoSign B = true /\ FClosed B. Lemma WfAx A : IsAx A -> Wf PeanoSign A. Proof. intros [ IN | (B & -> & HB & HB')]. - apply Wf_iff. unfold axioms_list in IN. simpl in IN. intuition; subst; reflexivity. - repeat split; unfold induction_schema; cbn. + rewrite nForall_check. cbn. rewrite !check_bsubst, HB; auto. + red. rewrite nForall_level. cbn. assert (level (bsubst 0 Zero B) <= level B). { apply level_bsubst'. auto. } assert (level (bsubst 0 (Succ(BVar 0)) B) <= level B). { apply level_bsubst'. auto. } omega with *. + apply nForall_fclosed. red. cbn. assert (FClosed (bsubst 0 Zero B)). { red. rewrite bsubst_fvars. intro x. rewrite Names.union_spec. cbn. red in HB'. intuition. } assert (FClosed (bsubst 0 (Succ(BVar 0)) B)). { red. rewrite bsubst_fvars. intro x. rewrite Names.union_spec. cbn - [Names.union]. rewrite Names.union_spec. generalize (HB' x) (@Names.empty_spec x). intuition. } unfold FClosed in *. intuition. Qed. End PeanoAx. Local Open Scope string. Local Open Scope formula_scope. Definition PeanoTheory := {| sign := PeanoSign; IsAxiom := PeanoAx.IsAx; WfAxiom := PeanoAx.WfAx |}. (** Useful lemmas so as to be able to write proofs that take less than 1000 lines. *) Import PeanoAx. Lemma Symmetry : forall logic A B Γ, BClosed A -> BClosed B -> In ax2 Γ -> Pr logic (Γ ⊢ A = B) -> Pr logic (Γ ⊢ B = A). Proof. intros. apply R_Imp_e with (A := A = B); [ | assumption ]. assert (AX2 : Pr logic (Γ ⊢ ax2)). { apply R_Ax. exact H1. } unfold ax2 in AX2. apply R_All_e with (t := A) in AX2; [ | assumption ]. apply R_All_e with (t := B) in AX2; [ | assumption ]. cbn in AX2. assert (bsubst 0 B (lift A) = A). { assert (lift A = A). { apply lift_nop. exact H. } rewrite H3. apply bclosed_bsubst_id. exact H. } rewrite H3 in AX2. exact AX2. Qed. Lemma Transitivity : forall logic A B C Γ, BClosed A -> BClosed B -> BClosed C -> In ax3 Γ -> Pr logic (Γ ⊢ A = B) -> Pr logic (Γ ⊢ B = C) -> Pr logic (Γ ⊢ A = C). Proof. intros. apply R_Imp_e with (A := A = B /\ B = C); [ | apply R_And_i; assumption ]. assert (AX3 : Pr logic (Γ ⊢ ax3)). { apply R_Ax. exact H2. } unfold ax3 in AX3. apply R_All_e with (t := A) in AX3; [ | assumption ]. apply R_All_e with (t := B) in AX3; [ | assumption ]. apply R_All_e with (t := C) in AX3; [ | assumption ]. cbn in AX3. assert (bsubst 0 C (lift B) = B). { assert (lift B = B). {apply lift_nop. assumption. } rewrite H5. apply bclosed_bsubst_id. assumption. } rewrite H5 in AX3. assert (bsubst 0 C (bsubst 1 (lift B) (lift (lift A))) = A). { assert (lift A = A). { apply lift_nop. assumption. } rewrite H6. rewrite H6. assert (lift B = B). { apply lift_nop. assumption. } rewrite H7. assert (bsubst 1 B A = A). { apply bclosed_bsubst_id. assumption. } rewrite H8. apply bclosed_bsubst_id. assumption. } rewrite H6 in AX3. assumption. Qed. Lemma Hereditarity : forall logic A B Γ, BClosed A -> BClosed B -> In ax4 Γ -> Pr logic (Γ ⊢ A = B) -> Pr logic (Γ ⊢ Succ A = Succ B). Proof. intros. apply R_Imp_e with (A := A = B); [ | assumption ]. assert (AX4 : Pr logic (Γ ⊢ ax4)). { apply R_Ax. assumption. } unfold ax4 in AX4. apply R_All_e with (t := A) in AX4; [ | assumption ]. apply R_All_e with (t := B) in AX4; [ | assumption ]. cbn in AX4. assert (bsubst 0 B (lift A) = A). { assert (lift A = A). { apply lift_nop. assumption. } rewrite H3. apply bclosed_bsubst_id. assumption. } rewrite H3 in AX4. assumption. Qed. Lemma AntiHereditarity : forall logic A B Γ, BClosed A -> BClosed B -> In ax13 Γ -> Pr logic (Γ ⊢ Succ A = Succ B) -> Pr logic (Γ ⊢ A = B). Proof. intros. apply R_Imp_e with (A := Succ A = Succ B); [ | assumption ]. assert (AX13 : Pr logic (Γ ⊢ ax13)). { apply R_Ax. assumption. } unfold ax13 in AX13. apply R_All_e with (t := A) in AX13; [ | assumption ]. apply R_All_e with (t := B) in AX13; [ | assumption ]. cbn in AX13. assert (bsubst 0 B (lift A) = A). { assert (lift A = A). { apply lift_nop. assumption. } rewrite H3. apply bclosed_bsubst_id. assumption. } rewrite H3 in AX13. assumption. Qed. Ltac axiom ax name := match goal with | |- Pr ?l (?ctx ⊢ _) => assert (name : Pr l (ctx ⊢ ax)); [ apply R_Ax; compute; intuition | ]; unfold ax in name end. Ltac app_R_All_i t := apply R_All_i with (x := t); [ rewrite<- Names.mem_spec; now compute | ]. Ltac eapp_R_All_i := eapply R_All_i; [ rewrite<- Names.mem_spec; now compute | ]. Ltac sym := apply Symmetry; [ auto | auto | compute; intuition | ]. Ltac ahered := apply Hereditarity; [ auto | auto | compute; intuition | ]. Ltac hered := apply AntiHereditarity; [ auto | auto | compute; intuition | ]. Ltac trans b := apply Transitivity with (B := b); [ auto | auto | auto | compute; intuition | | ]. Ltac thm := unfold IsTheorem; split; [ unfold Wf; split; [ auto | split; auto ] | ]. Ltac change_succ := match goal with | |- context[ Fun "S" [?t] ] => change (Fun "S" [t]) with (Succ (t)); change_succ | _ => idtac end. Ltac cbm := cbn; change (Fun "O" []) with Zero; change_succ. Ltac parse term := match term with | (_ -> ?queue)%form => parse queue | (∀ ?formula)%form => formula end. Ltac rec := match goal with | |- exists axs, (Forall (IsAxiom PeanoTheory) axs /\ Pr ?l (axs ⊢ ?A))%type => let form := parse A in exists (induction_schema form :: axioms_list); set (Γ := induction_schema form :: axioms_list); set (rec := induction_schema form); split; [ apply Forall_forall; intros x H; destruct H; [ simpl; unfold IsAx; right; exists form ; split; [ auto | split; [ auto | auto ]] | simpl; unfold IsAx; left; assumption ] | repeat apply R_Imp_i; eapply R_Imp_e; [ apply R_Ax; unfold induction_schema; cbm; intuition | simpl; apply R_And_i; cbn ] ]; cbm (* | _ => idtac *) end. (** Some basic proofs in Peano arithmetics. *) Lemma ZeroRight : IsTheorem Intuiti PeanoTheory (∀ (#0 = #0 + Zero)). Proof. thm. rec. + app_R_All_i "y". cbm. sym. axiom ax9 AX9. apply R_All_e with (t := Zero) in AX9; auto. + app_R_All_i "y". cbm. apply R_Imp_i. set (H1 := FVar _ = _). sym. trans (Succ ((FVar "y") + Zero)). - axiom ax10 AX10. apply R_All_e with (t := FVar "y") in AX10; auto. apply R_All_e with (t := Zero) in AX10; auto. - ahered. sym. apply R_Ax. apply in_eq. Qed. Lemma SuccRight : IsTheorem Intuiti PeanoTheory (∀∀ (Succ(#1 + #0) = #1 + Succ(#0))). Proof. thm. rec. + app_R_All_i "x". app_R_All_i "y". cbm. sym. trans (Succ (FVar "y")). - axiom ax9 AX9. apply R_All_e with (t := Succ (FVar "y")) in AX9; auto. - ahered. sym. axiom ax9 AX9. apply R_All_e with (t := FVar "y") in AX9; auto. + app_R_All_i "x". cbm. apply R_Imp_i. app_R_All_i "y". cbm. set (hyp := ∀ Succ _ = _). trans (Succ (Succ (FVar "x" + FVar "y"))). - ahered. axiom ax10 AX10. apply R_All_e with (t := FVar "x") in AX10; auto. apply R_All_e with (t := FVar "y") in AX10; auto. - trans (Succ (FVar "x" + Succ (FVar "y"))). * ahered. axiom hyp Hyp. apply R_All_e with (t := FVar "y") in Hyp; auto. * axiom ax10 AX10. sym. apply R_All_e with (t := FVar "x") in AX10; auto. apply R_All_e with (t := Succ (FVar "y")) in AX10; auto. Qed. Lemma Comm : IsTheorem Intuiti PeanoTheory ((∀ #0 = #0 + Zero) -> (∀∀ Succ(#1 + #0) = #1 + Succ(#0)) -> (∀∀ #0 + #1 = #1 + #0)). Proof. thm. rec; set (Γ' := _ :: _ :: Γ). + app_R_All_i "x". cbm. app_R_All_i "x". cbm. trans (FVar "x"). - sym. assert (Pr Intuiti (Γ' ⊢ ∀ # 0 = # 0 + Zero)). { apply R_Ax. simpl in *; intuition. } apply R_All_e with (t := FVar "x") in H; auto. - sym. axiom ax9 AX9. apply R_All_e with (t := FVar "x") in AX9; auto. + app_R_All_i "y". cbm. apply R_Imp_i. app_R_All_i "x". cbm. trans (Succ (FVar "x" + FVar "y")). - sym. assert (Pr Intuiti ((∀ # 0 + FVar "y" = FVar "y" + # 0) :: Γ' ⊢ ∀ ∀ Succ (#1 + #0) = #1 + Succ (#0))). { apply R_Ax. simpl in *; intuition. } apply R_All_e with (t := FVar "x") in H; auto. apply R_All_e with (t := FVar "y") in H; auto. - trans (Succ (FVar "y" + FVar "x")). * ahered. assert (Pr Intuiti ((∀ #0 + FVar "y" = FVar "y" + #0) :: Γ' ⊢ ∀ #0 + FVar "y" = FVar "y" + #0)). { apply R_Ax. apply in_eq. } apply R_All_e with (t := FVar "x") in H; auto. * sym. axiom ax10 AX10. apply R_All_e with (t := FVar "y") in AX10; auto. apply R_All_e with (t := FVar "x") in AX10; auto. Qed. Lemma Commutativity : IsTheorem Intuiti PeanoTheory (∀∀ #0 + #1 = #1 + #0). Proof. apply ModusPonens with (A := (∀∀ Succ(#1 + #0) = #1 + Succ(#0))). + apply ModusPonens with (A := ∀ #0 = #0 + Zero). * apply Comm. * apply ZeroRight. + apply SuccRight. Qed. (** A Coq model of this Peano theory, based on the [nat] type *) Definition PeanoFuns : modfuns nat := fun f => if f =? "O" then Some (existT _ 0 0) else if f =? "S" then Some (existT _ 1 S) else if f =? "+" then Some (existT _ 2 Nat.add) else if f =? "*" then Some (existT _ 2 Nat.mul) else None. Definition PeanoPreds : modpreds nat := fun p => if p =? "=" then Some (existT _ 2 (@Logic.eq nat)) else None. Lemma PeanoFuns_ok s : funsymbs PeanoSign s = get_arity (PeanoFuns s). Proof. unfold PeanoSign, peano_sign, PeanoFuns. simpl. unfold eqb, eqb_inst_string. repeat (case string_eqb; auto). Qed. Lemma PeanoPreds_ok s : predsymbs PeanoSign s = get_arity (PeanoPreds s). Proof. unfold PeanoSign, peano_sign, PeanoPreds. simpl. unfold eqb, eqb_inst_string. case string_eqb; auto. Qed. Definition PeanoPreModel : PreModel nat PeanoTheory := {| someone := 0; funs := PeanoFuns; preds := PeanoPreds; funsOk := PeanoFuns_ok; predsOk := PeanoPreds_ok |}. Lemma PeanoAxOk A : IsAxiom PeanoTheory A -> forall genv, interp_form PeanoPreModel genv [] A. Proof. unfold PeanoTheory. simpl. unfold PeanoAx.IsAx. intros [IN|(B & -> & CK & CL)]. - compute in IN. intuition; subst; cbn; intros; subst; omega. - intros genv. unfold PeanoAx.induction_schema. apply interp_nforall. intros stk Len. rewrite app_nil_r. cbn. intros (Base,Step). (* The Peano induction emulated by a Coq induction :-) *) induction m. + specialize (Base 0). apply -> interp_form_bsubst_gen in Base; simpl; eauto. + apply Step in IHm. apply -> interp_form_bsubst_gen in IHm; simpl; eauto. now intros [|k]. Qed. Definition PeanoModel : Model nat PeanoTheory := {| pre := PeanoPreModel; AxOk := PeanoAxOk |}.