Mercurial > cpdt > repo

comparison src/CpdtTactics.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 ed829eaa91b2
children
comparison
equal deleted inserted replaced
573:c3d77f2bb92c 574:1dc1d41620b6
5 * Unported License. 5 * Unported License.
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 Require Import Eqdep List Omega. 10 Require Import Eqdep List Lia.
11 11
12 Set Implicit Arguments. 12 Set Implicit Arguments.
13 13
14 14
15 (** A version of [injection] that does some standard simplifications afterward: clear the hypothesis in question, bring the new facts above the double line, and attempt substitution for known variables. *) 15 (** A version of [injection] that does some standard simplifications afterward: clear the hypothesis in question, bring the new facts above the double line, and attempt substitution for known variables. *)
194 || appHyps ltac:(fun L => inster L L)); 194 || appHyps ltac:(fun L => inster L L));
195 (** ...and then simplifying hypotheses. *) 195 (** ...and then simplifying hypotheses. *)
196 repeat (simplHyp invOne; intuition)); un_done 196 repeat (simplHyp invOne; intuition)); un_done
197 end; 197 end;
198 sintuition; rewriter; sintuition; 198 sintuition; rewriter; sintuition;
199 (** End with a last attempt to prove an arithmetic fact with [omega], or prove any sort of fact in a context that is contradictory by reasoning that [omega] can do. *) 199 (** End with a last attempt to prove an arithmetic fact with [lia], or prove any sort of fact in a context that is contradictory by reasoning that [lia] can do. *)
200 try omega; try (elimtype False; omega)). 200 try lia; try (elimtype False; lia)).
201 201
202 (** [crush] instantiates [crush'] with the simplest possible parameters. *) 202 (** [crush] instantiates [crush'] with the simplest possible parameters. *)
203 Ltac crush := crush' false fail. 203 Ltac crush := crush' false fail.
204 204
205 (** * Wrap Program's [dependent destruction] in a slightly more pleasant form *) 205 (** * Wrap Program's [dependent destruction] in a slightly more pleasant form *)