Skip to content

A quick reference for mapping Coq tactics to Lean tactics

Notifications You must be signed in to change notification settings

jldodds/coq-lean-cheatsheet

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

31 Commits
 
 
 
 
 
 
 
 

Repository files navigation

Coq to Lean Tactic Cheatsheet

This is a guide for coq users getting into writing lean proofs.

Please PR your own or request additions via issue tracker or lean gitter.

n/a doesn't mean it doesn't exist, only that I don't know about it.

The main table is for the Lean release v3.3.0.

Coq Tactic Lean Tactic Notes
; ;
 .       ,
assumption assumption      
admit admit
apply apply lean apply is coq eapply
apply H in A have A2 := H A Will create a new hypothesis A2, and A will persist, see coq-tactic-substitutes.lean for a closer approximation
assert have
auto n/a
autorewrite n/a simp using <attribute> approximates
change change
change with n/a
clear clear no clear -
constructor constructor
destruct cases
destruct x eqn:? destruct x
eapply apply
exact exact
exfalso exfalso
exists existsi use is the same, but takes the expected type into account. use requires mathlib
eexists existsi _
f_equal congr' 1 requires mathlib
fail fail_if_success {skip}
first [A | B |.. | X] first [A B .. X]
generalize t generalize : t = y y is name of the new variable, the name must be provided
generalize dependent revert
idtac skip skip does not print, succeeds trivially
induction induction
intro intro
intros intros
intuition n/a
inversion cases Cases should be applied to dependent arguments first
left left
omega omega requires mathlib. Might not have the same features as Coq's omega
pose let
pose proof have
progress n/a lean tactics by convention should fail if they don't progress
remember x as y eqn:h generalize h : x = y names must be provided
revert n/a always dependent
revert dependent revert
rewrite rewrite, rw
rewrite <- rewrite <-, rw
right right
simpl dsimp to some approximation at least. simp only might be closer
simpl in dsimp at
simpl in * dsimp at *
solve solve1
specialize (H e) specialize (H e)
split split
subst x subst x
subst n/a
symmetry symmetry
transitivity transitivity
trivial trivial
try T try {T} curly braces required
typeclasses eauto apply_instance
unfold unfold
unfold in unfold at
unshelve eapply fapply

Similar options from Coq exist in Lean as well. Whereas Coq options are set and unset with the Vernacular Set option and Unset option, Lean options toggled with set_option <option> true and set_option <option> false. Here is a list of Coq options and their Lean versions:

Coq option Lean option Notes
Printing Implicit pp.implicit default false
Printing Universes pp.universes default false
Printing Notations pp.notation default true

And other Vernacular:

Coq Vernacular Lean directive Notes
Opaque ident attribute [irreducible] ident
Transparent ident attribute [reducible] ident
Check term #check term
Print term #print term Can also be used to print structures, inductive types, notation
Proof using P include P include P makes P available to all proofs, as well as typeclass resolution if it is an instance. omit P un-includes P

Variables and sections

Coq construct Lean construct Notes
Variable parameter only within a section. Lean variable does not automatically apply arguments within the section
Universes universes use universe variables if you want to declare the universes, but not fix them for the file

About

A quick reference for mapping Coq tactics to Lean tactics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Contributors 3

  •  
  •  
  •  

Languages