Peano.v 12.3 KB
Newer Older
1

2
3
4
5
6
(** * 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 *)

7
8
Require Import Defs NameProofs Mix Meta.
Require Import Wellformed Theories Nary PreModels Models.
9
10
Import ListNotations.
Local Open Scope bool_scope.
11
Local Open Scope string_scope.
12
13
Local Open Scope eqb_scope.

14
15
16
17
(** The Peano axioms *)

Definition PeanoSign := Finite.to_infinite peano_sign.

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

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

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

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

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

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

Local Close Scope formula_scope.

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

71
Lemma WCAx A : IsAx A -> WC PeanoSign A.
72
73
Proof.
 intros [ IN | (B & -> & HB & HB')].
74
 - apply wc_iff. revert A IN. now apply forallb_forall.
75
76
 - 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
91
Local Open Scope formula_scope.

92
Definition PeanoTheory :=
93
 {| sign := PeanoSign;
94
    IsAxiom := PeanoAx.IsAx;
95
    WCAxiom := PeanoAx.WCAx |}.
96

97
(** 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
98

99
100
Import PeanoAx.

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

119
120
121
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).
122
123
124
125
Proof.
  intros.
  apply R_Imp_e with (A := A = B /\ B = C); [ | apply R_And_i; assumption ].
  assert (AX3 : Pr logic (Γ  ax3)).
126
  { apply R_Ax. exact H1. }
127
  unfold ax3 in AX3.
128
129
130
  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.
131
  cbn in AX3.
Pierre Letouzey's avatar
Pierre Letouzey committed
132
133
  assert (bsubst 0 C (lift 0 B) = B).
  { assert (lift 0 B = B). {apply lift_nop. assumption. } rewrite H4. apply bclosed_bsubst_id. assumption. }
134
  rewrite H4 in AX3.
Pierre Letouzey's avatar
Pierre Letouzey committed
135
136
137
  assert (bsubst 0 C (bsubst 1 (lift 0 B) (lift 0 (lift 0 A))) = A).
  { assert (lift 0 A = A). { apply lift_nop. assumption. } rewrite H5. rewrite H5.
    assert (lift 0 B = B). { apply lift_nop. assumption. } rewrite H6.
138
    assert (bsubst 1 B A = A). { apply bclosed_bsubst_id. assumption. } rewrite H7.
139
    apply bclosed_bsubst_id. assumption. }
140
  rewrite H5 in AX3.
141
142
143
  assumption.
Qed.

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

163
164
165
Lemma AntiHereditarity :
  forall logic A B Γ, BClosed A -> In ax13 Γ -> Pr logic (Γ  Succ A = Succ B) ->
                      Pr logic (Γ  A = B).
166
167
168
169
170
171
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.
172
173
  apply R_All_e with (t := A) in AX13.
  apply R_All_e with (t := B) in AX13.
174
  cbn in AX13.
Pierre Letouzey's avatar
Pierre Letouzey committed
175
176
  assert (bsubst 0 B (lift 0 A) = A).
  { assert (lift 0 A = A). { apply lift_nop. assumption. } rewrite H2.
177
    apply bclosed_bsubst_id. assumption. }
178
  rewrite H2 in AX13.
179
180
181
  assumption.
Qed.

182
183
184
185
186
187
188
189
190
191
192
193
194
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.

195
Lemma rec0_rule l Γ A_x :
196
  BClosed ( A_x) ->
197
198
199
200
  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).
201
202
203
204
205
206
207
208
209
210
211
212
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.
213
    * set (v := fresh (fvars (Γ   bsubst 0 Zero A_x)%form)).
214
215
216
217
218
219
220
221
222
223
224
225
      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
226
227
228
229
230
231
232
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.

233
Ltac calc :=
234
  match goal with
235
236
237
238
  | |- BClosed _ => reflexivity
  | |- In _ _ => rewrite <- list_mem_in; reflexivity
  | |- ~Names.In _ _ => rewrite<- Names.mem_spec; now compute
  | _ => idtac
239
  end.
240

241
242
243
Ltac inst H l :=
  match l with
  | [] => idtac
244
  | (?u::?l) => apply R_All_e with (t := u) in H; inst H l
245
  end.
246

247
248
249
250
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.
251

252
253
Ltac inst_axiom ax l :=
 let H := fresh in
254
 axiom ax H; inst H l; try easy.
255

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

259
Ltac sym := apply Symmetry; calc.
260

261
Ltac ahered := apply Hereditarity; calc.
262

263
Ltac hered := apply AntiHereditarity; calc.
264

265
266
Ltac trans b := apply Transitivity with (B := b); calc.

267
Ltac thm := unfold IsTheorem; split; [ now apply wc_iff | ].
268

269
270
271
272
273
274
Ltac parse term :=
  match term with
  | (_ -> ?queue)%form => parse queue
  | ( ?formula)%form => formula
  end.

275
Ltac rec :=
276
  match goal with
277
278
  | |- exists axs, (Forall (IsAxiom PeanoTheory) axs /\ Pr ?l (axs  ?A))%type => 
    let form := parse A in  
279
280
    exists (induction_schema form :: axioms_list); set (rec := induction_schema form); set (Γ := rec :: axioms_list); split;
      [ apply IsAx_adhoc; auto |
281
        repeat apply R_Imp_i;
282
        apply rec0_rule; calc ]; cbn
283
    (* | _ => idtac *)
284
  end.
285

286
            
287
288
(** Some basic proofs in Peano arithmetics. *)

289
Lemma ZeroRight :
290
  IsTheorem J PeanoTheory
291
            ( (#0 = #0 + Zero)).
292
293
294
Proof.
 thm.
 rec.
295
296
297
298
 + sym.
   inst_axiom ax9 [Zero].
 + app_R_All_i "y" y.
   apply R_Imp_i. set (H1 := _ = _).
299
   sym.
300
301
   trans (Succ (y + Zero)).
   - inst_axiom ax10 [y; Zero].
302
303
304
305
   - ahered.
     sym.
     apply R_Ax.
     apply in_eq.
306
Qed.
Samuel Ben Hamou's avatar
Samuel Ben Hamou committed
307

308
Lemma SuccRight : IsTheorem J PeanoTheory (∀∀ (Succ(#1 + #0) = #1 + Succ(#0))).
Samuel Ben Hamou's avatar
Samuel Ben Hamou committed
309
Proof.
310
311
  thm.
  rec.
312
  + app_R_All_i "y" y.
313
    sym.
314
315
    trans (Succ y).
    - inst_axiom ax9 [Succ y].
316
317
    - ahered.
      sym.
318
319
      inst_axiom ax9 [y].
  + app_R_All_i "x" x.
320
    apply R_Imp_i.
321
    app_R_All_i "y" y. fold x.
322
    set (hyp :=  Succ _ = _).
323
    trans (Succ (Succ (x + y))).
324
    - ahered.
325
326
      inst_axiom ax10 [x; y].
    - trans (Succ (x + Succ y)).
327
      * ahered.
328
329
330
        inst_axiom hyp [y].
      * sym.
        inst_axiom ax10 [x; Succ y].
331
Qed.
332

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

363
Lemma Commutativity : IsTheorem J PeanoTheory (∀∀ #0 + #1 = #1 + #0).
364
365
366
367
368
369
370
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.
371

372
373
(** A Coq model of this Peano theory, based on the [nat] type *)

374
Definition PeanoFuns : string -> optnfun nat nat :=
375
  fun f =>
376
377
378
379
380
  if f =? "O" then NFun 0 0
  else if f =? "S" then NFun 1 S
  else if f =? "+" then NFun 2 Nat.add
  else if f =? "*" then NFun 2 Nat.mul
  else Nop.
381

382
Definition PeanoPreds : string -> optnfun nat Prop :=
383
  fun p =>
384
385
  if p =? "=" then NFun 2 Logic.eq
  else Nop.
386
387
388
389
390

Lemma PeanoFuns_ok s :
 funsymbs PeanoSign s = get_arity (PeanoFuns s).
Proof.
 unfold PeanoSign, peano_sign, PeanoFuns. simpl.
391
 repeat (case eqbspec; auto); congruence.
392
393
394
395
396
397
Qed.

Lemma PeanoPreds_ok s :
 predsymbs PeanoSign s = get_arity (PeanoPreds s).
Proof.
 unfold PeanoSign, peano_sign, PeanoPreds. simpl.
398
 repeat (case eqbspec; auto); congruence.
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
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)].
415
 - compute in IN. intuition; subst; cbn; intros; subst; omega.
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
 - 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 |}.