Idp Cheat Sheet
Download a blank fillable Idp Cheat Sheet in PDF format just by clicking the "DOWNLOAD PDF" button.
Open the file in any PDF-viewing software. Adobe Reader or any alternative for Windows or MacOS are required to access and complete fillable content.
Complete Idp Cheat Sheet with your personal data - all interactive fields are highlighted in places where you should type, access drop-down lists or select multiple-choice options.
Some fillable PDF-files have the option of saving the completed form that contains your own data for later use or sending it out straight away.
ADVERTISEMENT
1
2Cheat Sheet
Terminology
cmd=> /(_ x) h
rewrite
/= -[a]/(0+a) -/c.
Introduce h specialized to x
Simplify the goal, then change a into 0+a, finally fold back the local definition c
x : T
P : nat ->
Prop
a, b : nat
a, b : nat
Context
S :
{set
T}
P : nat ->
Prop
x : nat
c := b + 3 : nat
c := b + 3 : nat
xS : x
\in
S
x : nat
h : P x
=========
=========
======================
T he bar
===============
=================
true && (a == b + 3)
0 + a == c
(forall
n, P n) -> G
G
Goal
forall
y, y == x -> y
\in
S
apply: H.
Apply H to the current goal
Assumptions
Conclusion
Pushing to the stack
H : A -> B
=========
Top is the first assumption, y here
=========
Note: in the following cmd is not
or exact. Moreover we display the goal just
apply
A
B
before cmd is run.
Stack alternative name for the list of Assumptions
cmd: (x) y
case: ab.
Push y then push x on the stack. y is also cleared
Eliminate the conjunction or disjunction
Popping from the stack
x, y : nat
x : nat
ab : A /\ B
Note: in the following example we assume cmd does nothing, exactly like move, to
=========
px : P x
px : P x
=========
focus on the effect of the intro pattern.
A -> B -> G
=========
=========
G
cmd=> x px
Q x y
forall
x0 y, Q x0 y
Run cmd, then pop Top, put it in the context naming it x then pop the new Top
case: (leqP a b).
and names it px in the context
cmd: {-2}x (erefl x)
Reason by cases using the leqP spec lemma
Push the type of (erefl x), then push x on the stack binding all but the second
x : T
occurrence
=========
a, b : nat
a, b : nat
a, b : nat
px : P x
forall
x,
=========
=========
=========
=========
x : nat
P x -> Q x -> G
a <= b && b > a
true && false
false && true
x : nat
Q x -> G
=========
=========
elim: s.
forall
x0,
cmd=> [|x xs] //
P x
x0 = x -> P x0
Perform an induction on s
Run cmd, then reason by cases on Top. In the first breanch do nothing, in the sec-
ond one pop two assumptions naming then x nd xs. Then get rid of trivial goals.
cmd: _.+1 {px}
s : seq nat
=========
Note that, since only the first branch is trivial, one can write => [// | x xs]
=========
Clear px and generalize the goal with respect to the first match of the pattern _.+1
=========
forall
n s,
too. caveat :
Immediately after
and
it does not perform any case
case
elim
P [::]
P s
P s -> P (n :: s)
analysis, but can still introduce different names in different branches
x : nat
x : nat
elim/last_ind: s
px : P x
x : nat
=========
=========
Start an induction on s using the induction principle last_ind
=========
xs : seq nat
forall
x0, x < x0
x < x.+1
forall
s : seq nat,
=========
=========
0 < size s -> P s
0 < size (x :: xs) -> P (x ::
s : seq nat
=========
forall
s x,
xs)
=========
P [::]
P s ->
Proof commands
P s
cmd=> /andP[pa pb]
P (rcons s x)
Run cmd, then apply the view andP to Top, then destruct the conjuction and
rewrite
Eab (Exc b).
have
pa : P a.
introduce in the context the two parts naming the pa and pb
Rewrite with Eab left to right, then with Exc by instantiating the first argument
Open a new goal for P a. Once resolved introduce a new entry in the context for
with b
it named pa
pa : A
=========
pb : B
Eab : a = b
Eab : a = b
a : T
A && B -> C -> D
=========
Exc :
forall
x, x = c
Exc :
forall
x, x = c
a : T
a : T
pa : P a
C -> D
=========
=========
=========
=========
=========
P a
P c
G
P a
cmd=> /= {px}
G
Run cmd then simplify the goal then discard px from then context
rewrite
-Eab {}Eac.
by
[].
Rewrite with Eab right to left then with Eac left to right, finally clear Eac
x : nat
Prove the goal by trivial means, or fail
x : nat
px : P x
Eab : a = b
=========
Eab : a = b
=========
=========
Eac : a = c
Q x -> R x
=========
true && Q x -> R x
0 <= n
=========
P c
cmd=> [y -> {x}]
P b
exact: H.
Run cmd then destruct the existential, then introduce y, then rewrite with Top
Apply H to the current goal and then assert all remaining goals, if any, are trivial.
rewrite
/(_ && _).
left to right and discard the equation, then clear x
Equivalent to
by
apply: H.
Unfold the definition of &&
x : nat
y : nat
a : bool
a : bool
H : B
=========
=========
=========
=========
=========
(exists2
y, x = y & Q y)
Q y -> P y
a && a = a
if
a
then
a
else
false = a
B
-> P x
ADVERTISEMENT
0 votes
Related Articles
Related forms
Related Categories
Parent category: Education