Mercurial > cpdt > repo

comparison src/Reflection.v @ 572:a913f19955e2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update for Coq 8.11
author Adam Chlipala <adam@chlipala.net>
date Sun, 02 Feb 2020 10:46:14 -0500
parents 2c8c693ddaba
children
comparison
equal deleted inserted replaced
571:3fc43e261f67 572:a913f19955e2
384 384
385 (** * A Smarter Tautology Solver *) 385 (** * A Smarter Tautology Solver *)
386 386
387 (** Now we are ready to revisit our earlier tautology solver example. We want to broaden the scope of the tactic to include formulas whose truth is not syntactically apparent. We will want to allow injection of arbitrary formulas, like we allowed arbitrary monoid expressions in the last example. Since we are working in a richer theory, it is important to be able to use equalities between different injected formulas. For instance, we cannot prove [P -> P] by translating the formula into a value like [Imp (Var P) (Var P)], because a Gallina function has no way of comparing the two [P]s for equality. 387 (** Now we are ready to revisit our earlier tautology solver example. We want to broaden the scope of the tactic to include formulas whose truth is not syntactically apparent. We will want to allow injection of arbitrary formulas, like we allowed arbitrary monoid expressions in the last example. Since we are working in a richer theory, it is important to be able to use equalities between different injected formulas. For instance, we cannot prove [P -> P] by translating the formula into a value like [Imp (Var P) (Var P)], because a Gallina function has no way of comparing the two [P]s for equality.
388 388
389 To arrive at a nice implementation satisfying these criteria, we introduce the %\index{tactics!quote}%[quote] tactic and its associated library. *) 389 To arrive at a nice implementation satisfying these criteria, we introduce the %\index{tactics!quote}%[quote] tactic and its associated library. (Actually, this tactic has apparently gone away in the most recent Coq versions, so this section is of historic interest only.) *)
390 390
391 Require Import Quote. 391 (*Require Import Quote.
392 392
393 (* begin thide *) 393 (* begin thide *)
394 Inductive formula : Set := 394 Inductive formula : Set :=
395 | Atomic : index -> formula 395 | Atomic : index -> formula
396 | Truth : formula 396 | Truth : formula
652 H9) H7) H5) H3) H1) H 652 H9) H7) H5) H3) H1) H
653 : True /\ True /\ True /\ True /\ True /\ True /\ False -> False 653 : True /\ True /\ True /\ True /\ True /\ True /\ False -> False
654 ]] 654 ]]
655 655
656 The traditional [tauto] tactic introduces a quadratic blow-up in the size of the proof term, whereas proofs produced by [my_tauto] always have linear size. *) 656 The traditional [tauto] tactic introduces a quadratic blow-up in the size of the proof term, whereas proofs produced by [my_tauto] always have linear size. *)
657 *)
657 658
658 (** ** Manual Reification of Terms with Variables *) 659 (** ** Manual Reification of Terms with Variables *)
659 660
660 (* begin thide *) 661 (* begin thide *)
661 (** The action of the [quote] tactic above may seem like magic. Somehow it performs equality comparison between subterms of arbitrary types, so that these subterms may be represented with the same reified variable. While [quote] is implemented in OCaml, we can code the reification process completely in Ltac, as well. To make our job simpler, we will represent variables as [nat]s, indexing into a simple list of variable values that may be referenced. 662 (** The action of the [quote] tactic above may seem like magic. Somehow it performs equality comparison between subterms of arbitrary types, so that these subterms may be represented with the same reified variable. While [quote] is implemented in OCaml, we can code the reification process completely in Ltac, as well. To make our job simpler, we will represent variables as [nat]s, indexing into a simple list of variable values that may be referenced.