Mercurial > cpdt > repo

comparison src/GeneralRec.v @ 380:31fa03bc0f18

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Get it to build with Coq 8.4
author Adam Chlipala <adam@chlipala.net>
date Thu, 29 Mar 2012 18:10:52 -0400
parents d1276004eec9
children 05efde66559d
comparison
equal deleted inserted replaced
379:e23d41ae63be 380:31fa03bc0f18
1 (* Copyright (c) 2006, 2011, Adam Chlipala 1 (* Copyright (c) 2006, 2011-2012, Adam Chlipala
2 * 2 *
3 * This work is licensed under a 3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
344 344
345 Hint Resolve ex_irrelevant. 345 Hint Resolve ex_irrelevant.
346 346
347 Require Import Max. 347 Require Import Max.
348 348
349 Theorem max_spec_le : forall n m, n <= m /\ max n m = m \/ m <= n /\ max n m = n.
350 induction n; destruct m; simpl; intuition;
351 specialize (IHn m); intuition.
352 Qed.
353
349 Ltac max := intros n m; generalize (max_spec_le n m); crush. 354 Ltac max := intros n m; generalize (max_spec_le n m); crush.
350 355
351 Lemma max_1 : forall n m, max n m >= n. 356 Lemma max_1 : forall n m, max n m >= n.
352 max. 357 max.
353 Qed. 358 Qed.