Peano.v 12.3 KB
Newer Older
1

2
3
4
5
6
7
(** * 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.
8
9
10
11
Import ListNotations.
Local Open Scope bool_scope.
Local Open Scope eqb_scope.

12
13
14
15
(** The Peano axioms *)

Definition PeanoSign := Finite.to_infinite peano_sign.

16
17
Notation Zero := (Fun "O" []).
Notation Succ x := (Fun "S" [x]).
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37

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)).
38
Definition ax11 :=  (Zero * #0 = Zero).
39
40
41
42
43
44
Definition ax12 := ∀∀ (Succ(#1) * #0 = (#1 * #0) + #0).

Definition ax13 := ∀∀ (Succ(#1) = Succ(#0) -> #1 = #0).
Definition ax14 :=  ~(Succ(#0) = Zero).

Definition axioms_list :=
45
 [ ax1; ax2; ax3; ax4; ax5; ax6; ax7; ax8;
46
47
    ax9; ax10; ax11; ax12; ax13; ax14 ].

48
49
50
(** Beware, [bsubst] is ok below for turning [#0] into [Succ #0], but
    only since it contains now a [lift] of substituted terms inside
    quantifiers.
51
52
53
    And the unconventional [] before [A[0]] is to get the right
    bounded vars (Hack !). *)

54
55
56
Definition induction_schema A_x :=
  let A_0 := bsubst 0 Zero A_x in
  let A_Sx := bsubst 0 (Succ(#0)) A_x in
57
  nForall
58
59
    (Nat.pred (level A_x))
    ((( A_0) /\ ( (A_x -> A_Sx))) ->  A_x).
60
61
62
63
64
65

Local Close Scope formula_scope.

Definition IsAx A :=
  List.In A axioms_list \/
  exists B, A = induction_schema B /\
66
            check PeanoSign B = true /\
67
68
            FClosed B.

69
Lemma WfAx A : IsAx A -> Wf PeanoSign A.
70
71
72
73
74
75
76
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.
77
     rewrite !check_bsubst, HB; auto.
78
79
80
   + red. rewrite nForall_level. cbn.
     assert (level (bsubst 0 Zero B) <= level B).
     { apply level_bsubst'. auto. }
81
82
     assert (level (bsubst 0 (Succ(BVar 0)) B) <= level B).
     { apply level_bsubst'. auto. }
83
     omega with *.
84
85
   + apply nForall_fclosed. rewrite <- form_fclosed_spec in *.
     cbn. now rewrite !fclosed_bsubst, HB'.
86
87
88
89
Qed.

End PeanoAx.

90
Local Open Scope string.
91
92
Local Open Scope formula_scope.

93
Definition PeanoTheory :=
94
 {| sign := PeanoSign;
95
96
97
    IsAxiom := PeanoAx.IsAx;
    WfAxiom := PeanoAx.WfAx |}.

98
(** Useful lemmas so as to be able to write proofs that take less than 1000 lines. *)
Samuel Ben Hamou's avatar
Samuel Ben Hamou committed
99

100
101
Import PeanoAx.

102
Lemma Symmetry : forall logic A B Γ, BClosed A -> In ax2 Γ -> Pr logic (Γ  A = B) -> Pr logic (Γ  B = A).
103
104
105
106
Proof.
  intros.
  apply R_Imp_e with (A := A = B); [ | assumption ].
  assert (AX2 : Pr logic (Γ  ax2)).
107
  { apply R_Ax. exact H0. }
108
  unfold ax2 in AX2.
109
110
  apply R_All_e with (t := A) in AX2.
  apply R_All_e with (t := B) in AX2.
111
112
  cbn in AX2.
  assert (bsubst 0 B (lift A) = A).
113
114
  { assert (lift A = A). { apply lift_nop. exact H. } rewrite H2. apply bclosed_bsubst_id. exact H. }
  rewrite H2 in AX2.
115
116
117
  exact AX2.
Qed.

118
Lemma Transitivity : forall logic A B C Γ, BClosed A -> BClosed B -> In ax3 Γ -> Pr logic (Γ  A = B) -> Pr logic (Γ  B = C) -> Pr logic (Γ  A = C).
119
120
121
122
Proof.
  intros.
  apply R_Imp_e with (A := A = B /\ B = C); [ | apply R_And_i; assumption ].
  assert (AX3 : Pr logic (Γ  ax3)).
123
  { apply R_Ax. exact H1. }
124
  unfold ax3 in AX3.
125
126
127
  apply R_All_e with (t := A) in AX3.
  apply R_All_e with (t := B) in AX3.
  apply R_All_e with (t := C) in AX3.
128
129
  cbn in AX3.
  assert (bsubst 0 C (lift B) = B).
130
131
  { assert (lift B = B). {apply lift_nop. assumption. } rewrite H4. apply bclosed_bsubst_id. assumption. }
  rewrite H4 in AX3.
132
  assert (bsubst 0 C (bsubst 1 (lift B) (lift (lift A))) = A).
133
134
135
  { assert (lift A = A). { apply lift_nop. assumption. } rewrite H5. rewrite H5.
    assert (lift B = B). { apply lift_nop. assumption. } rewrite H6.
    assert (bsubst 1 B A = A). { apply bclosed_bsubst_id. assumption. } rewrite H7.
136
    apply bclosed_bsubst_id. assumption. }
137
  rewrite H5 in AX3.
138
139
140
  assumption.
Qed.

141
Lemma Hereditarity : forall logic A B Γ, BClosed A -> In ax4 Γ -> Pr logic (Γ  A = B) -> Pr logic (Γ  Succ A = Succ B).
142
143
144
145
146
147
Proof.
  intros.
  apply R_Imp_e with (A := A = B); [ | assumption ].
  assert (AX4 : Pr logic (Γ  ax4)).
  { apply R_Ax. assumption. }
  unfold ax4 in AX4.
148
149
  apply R_All_e with (t := A) in AX4.
  apply R_All_e with (t := B) in AX4.
150
151
  cbn in AX4.
  assert (bsubst 0 B (lift A) = A).
152
  { assert (lift A = A). { apply lift_nop. assumption. } rewrite H2.
153
    apply bclosed_bsubst_id. assumption. }
154
  rewrite H2 in AX4.
155
156
157
  assumption.
Qed.

158
Lemma AntiHereditarity : forall logic A B Γ, BClosed A -> In ax13 Γ -> Pr logic (Γ  Succ A = Succ B) -> Pr logic (Γ  A = B).
159
160
161
162
163
164
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.
165
166
  apply R_All_e with (t := A) in AX13.
  apply R_All_e with (t := B) in AX13.
167
168
  cbn in AX13.
  assert (bsubst 0 B (lift A) = A).
169
  { assert (lift A = A). { apply lift_nop. assumption. } rewrite H2.
170
    apply bclosed_bsubst_id. assumption. }
171
  rewrite H2 in AX13.
172
173
174
  assumption.
Qed.

175
176
177
178
179
180
181
182
183
184
185
186
187
Lemma IsAx_adhoc form :
  check PeanoSign form = true ->
  FClosed form ->
  Forall IsAx (induction_schema form ::axioms_list).
Proof.
  intros.
  apply Forall_forall.
  intros x Hx.
  destruct Hx.
  + simpl. unfold IsAx. right. exists form. split; [ auto | split; [ auto | auto ]].
  + simpl. unfold IsAx. left. assumption.
Qed.

188
Lemma rec0_rule l Γ A_x :
189
  BClosed ( A_x) ->
190
191
192
193
  In (induction_schema A_x) Γ ->
  Pr l (Γ  bsubst 0 Zero A_x) ->
  Pr l (Γ   (A_x -> bsubst 0 (Succ(#0)) A_x)) ->
  Pr l (Γ   A_x).
194
195
196
197
198
199
200
201
202
203
204
205
Proof.
  intros.
  eapply R_Imp_e.
  + apply R_Ax.
    unfold induction_schema in H0.
    unfold BClosed in H.
    cbn in H.
    rewrite H in H0.
    cbn in H0.
    apply H0.
  + simpl.
    apply R_And_i; cbn.
206
    * set (v := fresh (fvars (Γ   bsubst 0 Zero A_x)%form)).
207
208
209
210
211
212
213
214
215
216
217
218
      apply R_All_i with (x:=v).
      apply fresh_ok.
      rewrite form_level_bsubst_id.
      - assumption.
      - apply level_bsubst.
        ++ unfold BClosed in H. cbn in H; omega.
        ++ cbn; omega.
    * assumption.
Qed.

(* And tactics to make the proofs look like natural deduction proofs. *)

Samuel Ben Hamou's avatar
Samuel Ben Hamou committed
219
220
221
222
223
224
225
Ltac reIff :=
  match goal with
  | |- context [ ((?A -> ?B) /\ _ )%form ] => fold (Iff A B); reIff
  | H : context [ ((?A -> ?B) /\ _ )%form ] |- _ => fold (Iff A B) in H; reIff
  | _ => idtac
  end.

226
Ltac calc :=
227
  match goal with
228
229
230
231
  | |- BClosed _ => reflexivity
  | |- In _ _ => rewrite <- list_mem_in; reflexivity
  | |- ~Names.In _ _ => rewrite<- Names.mem_spec; now compute
  | _ => idtac
232
  end.
233

234
235
236
Ltac inst H l :=
  match l with
  | [] => idtac
237
  | (?u::?l) => apply R_All_e with (t := u) in H; inst H l
238
  end.
239

240
241
242
243
Ltac axiom ax name :=
  match goal with
    | |- Pr ?l (?ctx  _) => assert (name : Pr l (ctx  ax)); [ apply R_Ax; calc | ]; unfold ax in name
  end.
244

245
246
Ltac inst_axiom ax l :=
 let H := fresh in
247
 axiom ax H; inst H l; try easy.
248

Samuel Ben Hamou's avatar
Samuel Ben Hamou committed
249
Ltac app_R_All_i t v := apply R_All_i with (x := t); calc; cbn; set (v := FVar t); reIff.
250
Ltac eapp_R_All_i := eapply R_All_i; calc.
251

252
Ltac sym := apply Symmetry; calc.
253

254
Ltac ahered := apply Hereditarity; calc.
255

256
Ltac hered := apply AntiHereditarity; calc.
257

258
259
260
Ltac trans b := apply Transitivity with (B := b); calc.

Ltac thm := unfold IsTheorem; split; [ unfold Wf; split; [ auto | split; auto ] | ].
261

262
263
264
265
266
267
Ltac parse term :=
  match term with
  | (_ -> ?queue)%form => parse queue
  | ( ?formula)%form => formula
  end.

268
Ltac rec :=
269
  match goal with
270
271
  | |- exists axs, (Forall (IsAxiom PeanoTheory) axs /\ Pr ?l (axs  ?A))%type => 
    let form := parse A in  
272
273
    exists (induction_schema form :: axioms_list); set (rec := induction_schema form); set (Γ := rec :: axioms_list); split;
      [ apply IsAx_adhoc; auto |
274
        repeat apply R_Imp_i;
275
        apply rec0_rule; calc ]; cbn
276
    (* | _ => idtac *)
277
  end.
278

279
            
280
281
(** Some basic proofs in Peano arithmetics. *)

Samuel Ben Hamou's avatar
Samuel Ben Hamou committed
282
Lemma ZeroRight : IsTheorem Intuiti PeanoTheory ( (#0 = #0 + Zero)).
283
284
285
Proof.
 thm.
 rec.
286
287
288
289
 + sym.
   inst_axiom ax9 [Zero].
 + app_R_All_i "y" y.
   apply R_Imp_i. set (H1 := _ = _).
290
   sym.
291
292
   trans (Succ (y + Zero)).
   - inst_axiom ax10 [y; Zero].
293
294
295
296
   - ahered.
     sym.
     apply R_Ax.
     apply in_eq.
297
Qed.
Samuel Ben Hamou's avatar
Samuel Ben Hamou committed
298

299
Lemma SuccRight : IsTheorem Intuiti PeanoTheory (∀∀ (Succ(#1 + #0) = #1 + Succ(#0))).
Samuel Ben Hamou's avatar
Samuel Ben Hamou committed
300
Proof.
301
302
  thm.
  rec.
303
  + app_R_All_i "y" y.
304
    sym.
305
306
    trans (Succ y).
    - inst_axiom ax9 [Succ y].
307
308
    - ahered.
      sym.
309
310
      inst_axiom ax9 [y].
  + app_R_All_i "x" x.
311
    apply R_Imp_i.
312
    app_R_All_i "y" y. fold x.
313
    set (hyp :=  Succ _ = _).
314
    trans (Succ (Succ (x + y))).
315
    - ahered.
316
317
      inst_axiom ax10 [x; y].
    - trans (Succ (x + Succ y)).
318
      * ahered.
319
320
321
        inst_axiom hyp [y].
      * sym.
        inst_axiom ax10 [x; Succ y].
322
Qed.
323

324
325
Lemma Comm :
  IsTheorem Intuiti PeanoTheory
326
327
            (( #0 = #0 + Zero) -> (∀∀ Succ(#1 + #0) = #1 + Succ(#0)) ->
               (∀∀ #0 + #1 = #1 + #0)).
328
Proof.
329
  thm.
330
  rec; set (Γ' := _ :: _ :: Γ).
331
332
  + app_R_All_i "x" x.
    trans x.
333
    - sym.
334
335
      assert (Pr Intuiti (Γ'   # 0 = # 0 + Zero)). { apply R_Ax. calc. }
      apply R_All_e with (t := x) in H; auto.
336
    - sym.
337
338
      inst_axiom ax9 [x].
  + app_R_All_i "y" y.
339
    apply R_Imp_i.
340
341
    app_R_All_i "x" x.
    trans (Succ (x + y)).
342
    - sym.
343
344
345
346
      assert (Pr Intuiti (( #0 + y = y + #0) :: Γ'    Succ (#1 + #0) = #1 + Succ (#0))). { apply R_Ax. calc. }
      apply R_All_e with (t := x) in H; auto.
      apply R_All_e with (t := y) in H; auto.
    - trans (Succ (y + x)).
347
      * ahered.
348
        assert (Pr Intuiti (( #0 + y = y + #0) :: Γ'   #0 + y = y + #0)). { apply R_Ax. apply in_eq. }
349
        apply R_All_e with (t := x) in H; auto.
350
      * sym.
351
        inst_axiom ax10 [y; x].
352
Qed.
Samuel Ben Hamou's avatar
Samuel Ben Hamou committed
353

354
355
356
357
358
359
360
361
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.
362

363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
(** 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)].
408
 - compute in IN. intuition; subst; cbn; intros; subst; omega.
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
 - 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 |}.