Mercurial > cpdt > repo

comparison src/GeneralRec.v @ 574:1dc1d41620b6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Builds with Coq 8.15.2
author Adam Chlipala <adam@chlipala.net>
date Sun, 31 Jul 2022 14:48:22 -0400
parents a913f19955e2
children
comparison
equal deleted inserted replaced
573:c3d77f2bb92c 574:1dc1d41620b6
6 * The license text is available at: 6 * The license text is available at:
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *) 8 *)
9 9
10 (* begin hide *) 10 (* begin hide *)
11 Require Import Arith List Omega. 11 Require Import Arith List Lia.
12 12
13 Require Import Cpdt.CpdtTactics Cpdt.Coinductive. 13 Require Import Cpdt.CpdtTactics Cpdt.Coinductive.
14 14
15 Require Extraction. 15 Require Extraction.
16 16
161 length ls1 < length ls2. 161 length ls1 < length ls2.
162 162
163 (** We must prove that the relation is truly well-founded. To save some space in the rest of this chapter, we skip right to nice, automated proof scripts, though we postpone introducing the principles behind such scripts to Part III of the book. Curious readers may still replace semicolons with periods and newlines to step through these scripts interactively. *) 163 (** We must prove that the relation is truly well-founded. To save some space in the rest of this chapter, we skip right to nice, automated proof scripts, though we postpone introducing the principles behind such scripts to Part III of the book. Curious readers may still replace semicolons with periods and newlines to step through these scripts interactively. *)
164 164
165 Hint Constructors Acc. 165 Hint Constructors Acc.
166 166 Hint Extern 2 (Acc _ _) => lia.
167 Hint Extern 2 (_ <= _) => lia.
168
167 Lemma lengthOrder_wf' : forall len, forall ls, length ls <= len -> Acc lengthOrder ls. 169 Lemma lengthOrder_wf' : forall len, forall ls, length ls <= len -> Acc lengthOrder ls.
168 unfold lengthOrder; induction len; crush. 170 unfold lengthOrder; induction len; crush.
169 Defined. 171 Defined.
170 172
171 Theorem lengthOrder_wf : well_founded lengthOrder. 173 Theorem lengthOrder_wf : well_founded lengthOrder.
504 | S n' => f (Fix' n') x 506 | S n' => f (Fix' n') x
505 end. 507 end.
506 508
507 (** Now it is straightforward to package [Fix'] as a computation combinator [Fix]. *) 509 (** Now it is straightforward to package [Fix'] as a computation combinator [Fix]. *)
508 510
509 Hint Extern 1 (_ >= _) => omega. 511 Hint Extern 1 (_ >= _) => lia.
510 Hint Unfold leq. 512 Hint Unfold leq.
511 513
512 Lemma Fix'_ok : forall steps n x v, proj1_sig (Fix' n x) steps = Some v 514 Lemma Fix'_ok : forall steps n x v, proj1_sig (Fix' n x) steps = Some v
513 -> forall n', n' >= n 515 -> forall n', n' >= n
514 -> proj1_sig (Fix' n' x) steps = Some v. 516 -> proj1_sig (Fix' n' x) steps = Some v.