DSSS17 Slack Notes

Table of Contents

1 #coq

1.1 Introduction

This document is a summary of the #coq channel from the DeepSpec Summer School in 2017, originally summarized by Calvin Beck.

Special thanks to:

  • John Wiegley: setting up a ZNC bouncer to grab logs from IRC
  • Perry Metzger: setting up the VPS for the bouncer
  • All of the DSSS17 participants for their great questions and answers

If you wish to make contributions, changes, or corrections, please feel free to make a pull request.

1.2 Resources

1.2.1 General Coq   coq

1.2.2 Coq plugins   plugins

1.2.3 Ltac   ltac

1.2.4 ssreflect   ssreflect

1.2.6 Misc

1.3 Coq Libraries

1.4 Papers

1.6 Proof General   pg coq

Proof general is an Emacs interface to a number of proof assistants. In particular it works quite well with Coq!

https://proofgeneral.github.io/

1.6.1 Coq has frozen in proof general   bugs

Steps to fix proof-general when it gets stuck:

  • C-c C-c: proof-interrupt-process.
  • C-c C-u: proof-undo-last-successful-command.
  • C-c C-x: proof-shell-exit, follow this with C-c <C-return> to get back to the original point.
  • Open a shell and kill coqtop.

1.6.2 Use company coq

Company-coq is an Emacs mode on top of proof general which provides a lot of useful additions. It prettifies symbols (which can be turned off), it provides a lot of completions which can be very useful when discovering tactics, and it provides easy ways to look up types and documentation.

https://github.com/cpitclaudel/company-coq

1.6.3 MELPA?

Proof general is not on MELPA as of writing, but the plan is to have a MELPA package once the new proof general is out of beta.

1.6.4 coq-compile-before-require

http://proofgeneral.inf.ed.ac.uk/htmlshow.php?title=Proof+General+user+manual&file=releases/ProofGeneral/doc/ProofGeneral/ProofGeneral_12.html

Proof general will automatically compile files when a Require is executed if the coq-compile-before-require variable is set to t. This can be useful, and it should only recompile if necessary.

One potential issues is if you have different versions of a big library like CompCert lying around, then it might end up compiling when you don't expect it, and Require statements may take a long time to evaluate.

1.6.5 ProofGeneral saving contents of buffers   pg

Useful keybindings in ProofGeneral: C-c C-a r and C-c C-a g, for persisting the contents of the goal and response buffer in another, special buffer, which accumulate each such output.

1.6.6 ProofGeneral look up information about identifier   pg

C-c C-i will run check on the identifier at point.

1.6.7 Ltac Debugging in Proof General   ltac debugging pg

There is no integration of the Ltac debugger in proof general, but you can switch to the *coq* buffer to use the debugger directly.

1.7 Managing Coq installations

1.7.1 Switching between versions   versions coq

You may find yourself wanting to switch between versions of Coq. There are a couple of options for this:

  • opam switch
  • the nix package manager
  • GNU stow

1.8 VST   vst

1.8.1 entailer and cancel   tactics vst

VST has the tactics entailer and entailer!, which are used to solve separation logic goals of the form `_ |– _`.

The difference between entailer and entailer! is that the latter uses a heuristic, so it can solve the goal faster. Usually you try entailer!, and if it doesn't work you try entailer.

If it does not work,see if you can rewrite the goal to get something of the form A |-- A. If your goal is exactly A |-- A, then you can use the tactic cancel, which is to entailer what reflexivity is to auto.

1.8.2 entailer vs forward   tactics vst

If your goal has Entail or _ |-- _, then you likely use entailer, or entailer!.

If your goal has semax, then you do forward.

1.8.3 Strongest Post Condition Principle

VST is using the strongest post condition principle.

https://en.wikipedia.org/wiki/Predicate_transformer_semantics#Strongest_postcondition

Strongest postcondition means if you go forward in the program from this precondition, with this instruction I can be sure to end up in this postcondition.

Weakest precondition is going backward in the sequence of the program. From this postcondition, if we applied this instruction c, I can assume this properties where true before applying this c.

The advantage of the forward approach is that it is very close to symbolic execution, with things such as assignment.

1.9 Coq   coq

1.9.1 Is there a way to force Coq to treat names as constructors   errors

This question is asking if there is a mechanism in Coq for treating constructors differently, similar to in Haskell. In Haskell you are forced to use capital letters at the beginning of every constructor's identifier. This makes it so when pattern matching the compiler can easily distinguish between what looks like a constructor, and what should be a variable (everything that starts with a lower case letter). This can be useful for avoiding mistakes where you think you're matching on a specific constructor, say C, but are instead matching on all constructors and assigning it to a variable c.

Coq has no mechanism for making these distinctions, but you will often get error messages like… 

Error: This clause is redundant.

Since the variable match could be redundant.

1.9.2 nat and large numbers   errors

Large natural numbers may cause segfaults, since they can't fit in memory. The unary representation is really inefficient. In real-world Coq developments you may want to use more efficient representations, like Z instead.

1.9.3 Set vs. Type   theory

Set is smaller than Type, since Set : Type.

Put non-propositional things (things you want to extract) in Set where possible.

1.9.4 Variable and Generalizable Variable   typeclasses

Generalizable Variables has nothing to do with Variable.

Generalizable Variables says "allow the following variables to be automatically introduced by `{...}".

Variable introduces a new axiom with the given name into the scope that will be added as a parameter at the end of a section.

1.9.5 Real Numbers in Coq   reals numbers

For real analysis in Coq there are a few libraries:

1.9.6 {| ... |} vs { ... }   typeclasses

These both introduce dependent records, and should be the same.

1.9.7 debug auto   tactics auto

Using debug auto will show you what auto is doing.

1.9.8 Prop vs. bool   theory

Some people prefer the use of bool for decidable propositions over Prop, since if it's decidable you can have a boolean function which automatically decides the proposition. This is better for manipulating the proposition, excluded middle is immediate, and you can program with it "natively". Prop and bool.

You should also be able to convert to Prop if necessary.

1.9.9 cbn   tactics

"call by name"

https://coq.inria.fr/distrib/current/refman/proof-engine/tactics.html#coq:tacn.cbn

Meant to be a more predictable replacement for simpl.

1.9.11 dependent induction   tactics induction

https://coq.inria.fr/distrib/current/refman/proof-engine/detailed-tactic-examples.html#dependent-induction

You often need dependent induction when a type dependent on a term you’ve destructed. It will induce a dependency on the axiom JMeq, which can in most cases be avoided (though sometimes with considerable effort).

This comes up a lot if you use types like vector.

dependent induction does not always have to add the JMeq axiom, but it often does.

1.9.12 Search   search

Can search for notations by putting double quotes around the notation. This can be unexpected when notations are used to essentially just rename functions. E.g., 

Notation open e1 e2     := (open_exp_wrt_exp e1 e2).

More info on search:

https://quanttype.net/posts/2016-04-19-finding-that-lemma.html

Can be very helpful to search for conversions between data types, like so: 

Search (nat -> Z).

This snippet will find functions which convert between `nat` and `Z`.

1.9.13 Modules   modules

Best to check out the tutorial, and reference manual here:

  1. Module Types   modules

    A module type is the list of Parameter's an Axiom's

    Module types are kind of like an interface, specifying what you need to make something of that module type.

  2. Module Functors   modules functors

    Module functors (which are different from the Haskell notion of functors!) are modules that take module types as arguments. This is useful because the module functor can define proofs that depend on the interface specified by the module type, so the proofs don't need to be repeated.

    E.g., you can have a Module Type for Ord which specifies the less than or equal to operation. Instances of Ord could be natural numbers with the standard numerical less than or equal to operator, or something like strings with a lexicographical less than or equal to operator.

    These instance of Ord could then be passed to a Module functor Min which defines a function min between two elements, and some theorems on min with proofs. The definition of min and proofs of its theorems need only be specified once, and the module functor can be instantiated for any Ord module.

    1. Example usage

      Say I have a module type: 

      Module Type Equiv.
  Parameter t  : Type.
  Parameter eq : t -> t -> Prop.
  Axiom eq_refl  : forall x, eq x x.
  Axiom eq_sym   : forall x y, eq x y -> eq y x.
  Axiom eq_trans : forall x y z, eq x y -> eq y z -> eq x z.
End Equiv.

      If you would like to have a second signature that depends upon this one, then you can use functors. E.g., 

      Module Type Poset (EQ : Equiv) <: Equiv.
  Include EQ.

  Parameter order : EQ.t -> EQ.t -> Prop.
  Axiom order_refl    : forall x y, EQ.eq x y -> order x y.
  Axiom order_antisym : forall x y, order x y -> order y x -> EQ.eq x y.
  Axiom order_trans   : forall x y z, order x y -> order y z -> order x z.
End Poset.
  3. Module parameters / instantiation   modules

    What if you want to define a function which only depends on the interface of a Module Type, and does not need the actual instantiation? E.g., 

    Module Type Boo.
  Parameter t: Type.
  Parameter eqb: t -> t -> bool.
  Definition eq (a0 a1: t): Prop := if (eqb a0 a1) then True else False.
End Boo.

    We don't want to have to define eq in each instantiation of the Module Type, but Coq will force us to do this: 

    Module BooNat <: Boo.
  Definition t := nat.
  Definition eqb := Nat.eqb.
  Definition eq (a0 a1: t): Prop := if (eqb a0 a1) then True else False. (* <----------- Why :(? *)
End BooNat.

Module BooZ <: Boo.
  Definition t := Z.
  Definition eqb := Z.eqb.
  Definition eq (a0 a1: t): Prop := if (eqb a0 a1) then True else False. (* <----------- Why :(? *)
End BooZ.

    To get rid of this boilerplate you can define a module that depends on this module type; people who want to use your module+module type will still need an instantiation of the Module Type. For example, the FMap library requires you to not only import their module, but also provide an instantiation of the DecidableTypeEx module type.

  4. Module Advantages / Disadvantages   modules
    1. Advantages
      • "One advantage to modules over type classes is that you never have to repeat typeclass parameters. Even though you can ameliorate that with a Section, it doesn’t help when you need to open a different section in another file, but other than that, I prefer type classes in nearly every way"
    2. Disadvantages
      • This paper https://www.cs.cmu.edu/~amoertbe/papers/refinements.pdf argues against the use of modules in Coq
      • The "diamond problem"
        • "typeclasses allows me to use @ to override a descendent type at a particular use location, whereas with modules I would have to instantiate a whole other set of definitions for each variation"
        • for example of what the diamond problem even worse than normal is that due to generativity, if B depends on A and C depends on A, and then make a D that depends on B and C, you’ll often get errors about A.foo != A.foo, not realized that B.A.foo and C.A.foo have been generated as different definitions
        • whereas with typeclasses where you have defined members rather than typeclasses, you just have an equality witness that must be provided, but it’s fairly clear from the context (after turning on implicits) why the disconnect is happening
      • Example of some problems: https://gist.github.com/11bf3953995fe37a90f2c4caaeed5d62

      Generally speaking people seem to prefer typeclasses over modules.

1.9.14 Typeclasses   typeclasses

Typeclasses in Coq are similar to typeclasses in Haskell. Here are some resources for typeclasses:

1.9.15 Module / Typeclass Comparisons   typeclasses modules

  1. "The holy grail"

    Supposedly this paper describes the "holy grail" between modules and typeclasses. Might be worth a read if you're trying to figure out the pros and cons of each.

    https://www.cl.cam.ac.uk/~jdy22/papers/modular-implicits.pdf

1.9.16 Sections   sections

https://coq.inria.fr/refman/language/gallina-extensions.html#section-mechanism

  1. Hypothesis / Variable   sections

    Hypothesis lets you provide a proposition, without providing a proof in a section. This hypothesis then becomes an argument to every function / definition that uses it within the section.

    Variable works the same way. 

    Section S.
  Variable n : nat.
  Definition square : nat := n * n.
  Check square.
  (* square : nat *)
End S.
Check square.
(* square : nat -> nat *)

1.9.17 Hint Ordering / Priority   auto hints

Can you order things in a hint database? You could do this manually by stratifying hints into different databases, which you then order in a tactic…

A better solution might be to add hint priority values using Hint Extern

https://coq.inria.fr/refman/proof-engine/tactics.html#creating-hint-databases

1.9.18 Reordering subgoals   goals

Sometimes you want to work on goals in a different order than Coq.

  • Focus 2 would focus the second sub-goal.
  • You can admit a subgoal, and then when you're done the rest of the proof go back and replace the admit with a proof.
  • ssreflect has some combinators for this, you can write last first to handle the last goal first.
  • all:swap 1 2 will swap the position of sub-goals 1 and2
  • If they're sufficiently trivial, you can do generate_subgoals; [on_first | on_second | | on_fourth]
  • all:revgoals to reverse the order of goals.

It can be best to avoid reordering, however, as it can make proofs more fragile.

A lot of reordering tactics are documented here:

https://coq.inria.fr/distrib/current/refman/proof-engine/tactics.html#non-logical-tactics

1.9.19 Unshelve, unshelve <tactic>   tacticals eauto

unshelve eapply will work a little harder to introduce evars.

Generated goals, typically to resolve evars, are put on "the shelf" and are not visible at first.

Unshelve puts all shelved goals into a visible state, and unshelve <tactic> will do this for only the shelved goals created by <tactic>

https://github.com/ProofGeneral/PG/issues/30#issuecomment-173974922

1.9.20 Evar unshelving   eauto

Using eauto, you end up with ~evars that are shelved. You can use unshelve econstructor. before your tactic to get evar goals first.

1.9.21 Destruct notations   notation

You can do destruct on notations like this: 

destruct "[=]".

1.9.22 pattern term   tactics

https://coq.inria.fr/distrib/current/refman/proof-engine/tactics.html#coq:tacn.pattern

pattern x will abstract all occurrences of x, so for instance it will change x + 1 into (fun v => v + 1) x. This can be useful for some automation and applications, which are expecting function applications.

1.9.23 Custom induction principles   induction

https://coq.inria.fr/distrib/current/refman/proof-engine/tactics.html#coq:tacn.induction

You may define custom induction principles in Coq and use them with the induction tactic via: 

induction Blah using my_custom_ind

An example of a different induction principle is the one defined in Coq's list library for performing induction over lists in reverse order: 

Theorem rev_ind :
  forall P:list A -> Prop,
    P [] ->
    (forall (x:A) (l:list A), P l -> P (l ++ [x])) -> forall l:list A, P l.

A question brought up in the summer school was how to use a custom induction principle with additional premises on the induction variable. E.g., 

my_custom_ind :
  forall m P,
    P m ->
    (forall n, P (S n) -> P n) ->
    forall n, n <= m -> P n

The additional premise being n <= m. One solution is to apply the induction premise directly (with apply), rather than using induction.

You may also need to use pattern x so that apply can infer P easily.

1.9.24 Destructing multiple existential variables   destruct existentials

If you have multiple existentially qualified variables in a hypothesis, like: 

H : exists x y, P x y

Then you can destruct all of them like: 

destruct H as [x [y H]].

You could also use Ltac, like the following: 

Ltac destruct_ex := repeat match goal with
                           | [ H : exists _, _ |- _ ] => destruct H
                           end.

This works because exists x y, z is really exists x, exists y, z.

Another alternative is something like: 

repeat destruct H as [? H]

Where ? is used to generate fresh names.

1.9.25 Ltac naming   ltac

In Ltac you can give something an automatically generated fresh name with ? in an "intros list". An example of this is: 

destruct H as [? Hblah]

Using ? in this way is similar to using fresh to generate a new name, like so: 

let H' := fresh "H" in destruct H as [H' Hblah]

? may try to be smart about naming, like giving names starting with n to nat types.

1.9.26 Program environment   instance program_instance program_environment

https://coq.inria.fr/refman/addendum/program.html

You may encounter Program Instance instead of Instance, Program Fixpoint instead of Fixpoint, and so on.

The Program environment just offers a bit more magic. Program will infer a lot more, and will auto-solve goals. When writing functional programs in this environment, you can leave holes that can either be solved automatically, or filled in later. Any goals that remain can be solved with Next Obligation.

You can change which tactic is used to auto-solve goals with 

Local Obligation Tactic := ...

Which can be very handy.

1.9.28 Decidable equality and conditionals   dec_eq

eq_dec : forall x y : atom, {x = y} + {x <> y}

And == is notation for eq_dec a b.

Now suppose you end up with a goal like: 

u = (if x == x then u else blah)

Since x == x is just notation for eq_dec x x, you can do 

destruct (x == x)

which will split the goal into two, one with the hypothesis x = x, and the other with the hypothesis x <> x.

In the first case, where x = x the goal should be solvable (auto should be sufficient in this specific instance).

The second case, where x <> x, is solvable by contradiction.

Using destruct (_ == _) can be a bit annoying, since you end up splitting the goal, only to dismiss one with contradiction, so it may be more convenient to rewrite using a theorem like the following: 

Theorem eq_dec_refl {A : Type} `{EqDec_eq A} (x : A) : eq_dec x x = left eq_refl.
Proof.
  destruct (eq_dec x x); [|contradiction].
  f_equal; apply (Eqdep_dec.UIP_dec eq_dec).
Qed.

https://github.com/plclub/metalib/pull/10/files

(left is the first constructor of the sumbool type, so it is the equivalent of "true" for the if expression)

1.9.29 UIPDec   dec_eq

EqDep_dec.UIP_dec can be handy for avoiding the JMeq_eq axiom when you have decidability.

1.9.30 Generators   quickchick

For quickchick generators it should be possible to write generators for dependent products, like for instance you could generate sorted lists, and then use the fact that sort produces evidence for sorted

1.9.31 Minifier   tools

Jason Gross has a “minifier” for Coq programs that reveal bugs in the compiler, in order to produce better bug reports for the Coq team:

https://github.com/JasonGross/coq-tools/blob/master/find-bug.py .

It’s quite easy to use, provided you can reduce any external dependencies.

1.9.32 Sigma types   sigma existentials

You might run into a bunch of stuff with sig in it. This is usually short for sigma. Sigma types are dependent sum types, and are used for existential quantifiers.

So, things like proj2_sig are to get the second member of a propositional sigma. 

forall x : { a : T | P T }, (proj2_sig x : P (proj1_sig x))

proj1_sig gets the value, and proj2_sig gets you the witness to the proposition.

sigT is the same as sig, but it uses Type instead of Prop

1.9.33 .. problems in PG   bugs

On old versions of ProofGeneral accidentally typing .. after a tactic, and trying to run it would cause ProofGeneral to get stuck. This seems to have been fixed in recent versions.

Steps to fix proof-general when it gets stuck:

  • C-c C-c: proof-interrupt-process.
  • C-c C-u: proof-undo-last-successful-command.
  • C-c C-x: proof-shell-exit, follow this with C-c <C-return> to get back to the original point.
  • Open a shell and kill coqtop.

1.9.34 Replacing with A:=B   set

Suppose using set you end up with A := B in the context, and you want to rewrite using this.

  • unfold A, subst A, or replace A with B by reflexivity should rewrite A with B in the goal.
  • fold A should rewrite B with A in the goal.

1.9.35 Coqtop   bugs

Coqtop is a little annoying to use because it doesn't support editing a line as you're writing it. The alternative is to use something like rlwrap. Apparently some versions of rlwrap have bugs which make them unusable with Coqtop. A usable alternative is ledit.

1.9.36 In Depth Semicolons

The impression is that the semicolon operator, bar; foo, will run foo on all goals created by bar.

gfail fails even when there are no goals, so foo; gfail will actually fail, even if foo solves all goals, whereas foo; fail will succeeds.

Running tactics after a semicolon when there are no remaining goals makes a lot of sense, though. It's reasonable to want to print after running a tactic, for instance admit; idtac "hello!"

1.9.37 invertn   tactics plugins ltac

This came up in Adam Chlipala's lectures, and was solved with multiple Ltac definitions: 

Ltac invert  H := inversion H; clear H; subst. 
Ltac invert0 H := invert H; fail. 
Ltac invert1 H := invert0 H || (invert H; [ ]). 
Ltac invert2 H := invert1 H || (invert H; [ | ]). 
Ltac invert3 H := invert2 H || (invert H; [ | | ]).
Ltac invert4 H := invert2 H || (invert H; [ | | | ]).

The goal is to use inversion on a hypothesis only if it will create less than or equal to n subgoals.

Somebody wrote a Coq plugin to do this:

https://github.com/lemonidas/invertn_tactic

And eventually an Ltac solution emerged as well, which went through a number of iterations: 

Ltac invert_internal n H :=
  lazymatch n with
  | 0 => inversion H; clear H; subst
  | S ?n' => invert_internal n' H; let g := numgoals in guard g < n
  end.
Tactic Notation "invert" integer(n) constr(H) := invert_internal n H.

Which was then shortened to: 

Ltac invert_internal n H :=
  inversion H; subst; clear H;
  let g := numgoals
  in guard g <= n.

It was then suggested that for efficiency the subst and clear tactics should be moved to after the guard, since there's no need to run these tactics if the guard fails: 

Tactic Notation "invert" integer(n) constr(H) :=
  inversion H; let g := numgoals in guard g <= n; clear H; subst.

1.9.38 Inversion subst warning   ltac tactics best_practices

inversion H; subst; clear H is a common pattern, but sometimes does not lead to nice results since the subst can cause large substitutions, leading to a really complicated context. Another issue is that this can rewrite hypothesis that you want to keep in tact.

1.9.39 Ltac bug fixing   ltac

Adam Chlipala points out:

Let me just point out that "fixing bugs in the Ltac semantics" often forces significant amounts of code to be rewritten after extensive debugging.

1.9.40 Redefining Ltac   ltac

::= can be used to redefine existing Ltac definitions.

1.9.41 Cut   tactics

  • for whoever was asking earlier today about "cut" in ltac: there appears to be a hint form that automatically does a cut in the prolog sense of pruning the search tree. it uses (hold on to your hat) a regular expression over the path of hint-identifiers in the tree, to decide where to cut. it also only works currently in the typeclass proof search, not general proof search. but maybe they'll extend it someday.
  • oh wait I misunderstood; typeclass eauto is maybe generally-applicable?
  • yeah, it looks like typeclasses eauto with core will run the new proof engine on the core auto database, making it usable in contexts where you'd normally use auto. and then you can, yeah (guh) prune the tree with Hint Cut <regexp>.

1.9.42 Refine vs Exact   tactics

There are two similar tactics built into Coq, refine and exact. Both let the user supply a Gallina term which can satisfy a goal (if the term has a type that matches).

exact has to give a term which is complete and exactly matches the goal.

With refine the user can put holes in places which create subgoals. For instance you could destruct something like: 

refine (match something with
        | false => _
        | true => _
        end).

Which would give you a subgoal for each branch.

1.9.43 Congruence   tactic

https://coq.inria.fr/distrib/current/refman/proof-engine/tactics.html#coq:tacn.congruence

Congruence can usually solve goals where you only have to do rewriting.

1.9.44 || and +   ltac tacticals

|| and + are somewhat similar ways of combining tactics.

t1 || t2 runs t2 if t1 "doesn't do anything", which means that it does not change the proof state. So, for example auto || fail "auto failed" would fail iff auto did not do anything.

fail || t ≡ t and intros X || t ≡ intros X as you might expect, but idtac || t ≡ t

fail + t ≡ t and intros X + t ≡ intros X, as well as idtac + t ≡ idtac.

first [t1 | t2 | … | tN] is like t1 + t2 + … + tN, except for a minor detail with failure levels

1.9.45 Progress   tactics

To know what it means for a tactic to make progress, it might be illustrative to look at the progress tactic:

https://coq.inria.fr/distrib/current/refman/proof-engine/ltac.html#coq:tacn.progress

1.9.46 Extraction   extraction

Coq extraction takes Gallina to a languaged called mini-ml, which is then further transformed to other languages.

Main bit of the ocaml extraction (this isn't including support code for number representations and such):

https://github.com/coq/coq/blob/master/plugins/extraction/ocaml.ml

1.9.47 Undocumented tactics as of 8.5   tactics documentation

  • autoapply
  • autounfold_one
  • debug auto
  • debug eauto
  • debug trivial
  • dependent generalize_eqs
  • dependent generalize_eqs_vars
  • destauto
  • destruct_with_eqn
  • dfs eauto
  • generalize_eqs
  • generalize_eqs_vars
  • gintuition
  • goal
  • guard
  • head_of_constr
  • hget_evar
  • hresolve_core
  • info
  • info_auto
  • info_eauto
  • infoH
  • info_trivial
  • new auto
  • now
  • progress_evars
  • prolog
  • rec
  • rewrite_all
  • rewrite_db
  • setoid_etransitivity
  • simple subst
  • soft functional induction
  • specialize_eqs
  • substitute
  • unshelve
  • etransitivity
  • zify

1.9.48 Is there a way to turn off notations when printing?   notations

Sometimes notations can be confusing and get in the way, if you want to disable notations when Coq is printing out information you can try: 

Unset Printing Notations.

So, for instance: 

Unset Printing Notations.

Theorem foo :
  forall (a b : nat),
    a <= b -> a < b.

will print the goal as: 

forall (a b : nat) (_ : le a b), lt a b

instead of: 

forall a b : nat, a <= b -> a < b

1.9.49 Functional induction   tactics induction

https://coq.inria.fr/refman/user-extensions/proof-schemes.html

And in particular:

https://coq.inria.fr/refman/user-extensions/proof-schemes.html#generation-of-induction-principles-with-functional-scheme

Coq can auto-generate induction principles following the "shape" of a function.

This came up in context of this theorem for Redblack tree insertion, that inserting into a tree always gives you a non-empty tree, the proposed solution using functional induction was: 

Functional Scheme ins_ind := Induction for ins Sort Prop.
Functional Scheme balance_ind := Induction for balance Sort Prop.

Lemma ins_not_E': forall x vx s, ins x vx s <> E.
Proof.
  unfold not.
  intros x vx s He.
  functional induction (ins x vx s); eauto; try discriminate;
    match goal with
      H : balance ?a ?b ?c ?d ?e = _ |- _ ] =>
          functional induction (balance a b c d e);
          try discriminate; eauto
    end.
Qed.

Not shorter than the automation from the lecture but it requires less thinking, arguably.

1.9.50 match reverse   ltac

match reverse goal with matches hypothesis in the reverse order from a regular match. 

Ltac test_ltac :=
  match goal with
  | H : _ |- _ => idtac H
  end.

Ltac test_ltac_rev :=
  match reverse goal with
  | H : _ |- _ => idtac H
  end.

Theorem foo :
  forall (A B : Prop), True.
Proof.
  intros A B.
  test_ltac.
  test_ltac_rev.
Qed.

This will print B when test_ltac is run, and A when test_ltac_rev is run.

1.9.51 Notations for repeated patterns (like lists)   notation

https://coq.inria.fr/distrib/current/refman/user-extensions/syntax-extensions.html#notations-with-recursive-patterns

.. in notations lets you define repeated patterns that get expanded.

1.9.52 Proof with   tactics

You can use Proof with <tactic> where <tactic> is replaced by some tactic to make proofs a bit shorter.

Proof with t will cause t1... to behave like t1; t automatically. If you find yourself using t a lot in a proof, using Proof with t can make things shorter.

Here's a small example: 

Theorem easy_theorem:
  forall A (a : A),
    a = a.
Proof with auto.
  intros A a...
Qed.

Created: 2018-07-05 Thu 11:56

Validate