Fillable Idp Cheat Sheet (Page 2 of 2) in pdf

Reﬂect and views

"[ \/ P1 , P2 | P3 ]" := (or3 P1 P2 P3)

rewrite

{3}[in

pat1]lem1

"[ && b1 , b2 , .. , bn & c ]" :=

Like in

rewrite

pat1]lem1 but use the pattern inferred from lem1 to iden-

reflect P b

tify the sub terms of X to be rewritten. Of these terms, rewrite only the third one.

(b1 && (b2 && .. (bn && c) .. ))

States that P is logically equivalent to b

Example:

"[ || b1 , b2 , .. , bn | c ]" :=

rewrite

{3}[in

f _ X]E.

apply: (iffP V)

(b1 || (b2 || .. (bn || c) .. ))

Proves a reﬂection goal, applying the view lemma V to the propositional part of

E : a = c

"#| A |" := (card (mem A))

reflect. E.g. apply: (iffP idP)

=========

"n .-tuple" := (tuple_of n)

a + f a (a + a) = f a (a + a) + a

"’I_ n" := (ordinal n)

P :

Prop

P :

Prop

P :

Prop

"f1 =1 f2" := (eqfun f1 f2)

b : bool

E : a = c

"b1 (+) b2" := (addb b1 b2)

=============

=========

Notations for natural numbers: nat

reflect P b

b -> P

P -> b

a + f a (a + a) = f a (c + a) + a

apply/V1/V2

rewrite

pat1]lem1

"n .+1" := (succn n)

Prove boolean equalities by considering them as logical double implications. The

Like before, but override the pattern inferred from lem1 with e

"n .-1" := (predn n)

term V1 (resp. V2) is the view lemma applied to the left (resp. right) hand side.

rewrite

pat1]lem1

"m + n" := (addn m n)

E.g. apply/idP/negP

pat1]lem1 but match pat1[X := e] insted of just pat1

rewrite

"m - n" := (subn m n)

"m <= n" := (leq m n)

rewrite

/def1 -[pat]/term /=

b1 : bool

"m < n" := (m.+1 <= n)

Unfold all occurrences of def1. Then match the goal against pat and change all

b2 : bool

"m <= n <= p" := ((m <= n) && (n <= p))

its occurrences into term (pure computation). Last simplify the goal

=========

"m * n" := (muln m n)

b1 = ~~ b2

b1 -> ~ b2

~ b2 -> b1

rewrite

3?lem2 // {hyp} => x px

"n .*2" := (double n)

Rewrite from 0 to 3 times with lem2, then try to solve with

[] all the goals.

rewrite: (eqP Eab)

"m ^ n" := (expn m n)

Finally clear hyp and introduce x and px

rewrite with the boolean equality Eab

"n ‘!" := (factorial n)

"m %/ d" := (divn m d)

Eab : a == b

"m %% d" := (modn m d)

Pattern matching detailed rules

=============

=========

"m == n %[mod d ]" := (m %% d == n %% d)

P a

P b

pattern a term, possibly containing _

"m %| d" := (dvdn m d)

"pi .-nat" := (pnat pi)

key The head symbol of a pattern

Idioms

Notations for lists: seq T

The sub terms selected by a pattern:

case: b => [h1| h2 h3]

"x :: s" := (cons _ x s)

Push b, reason by cases, then pop h1 in the ﬁrst branch and h2 and h3 in the

1. the goal is traversed outside in, left to right, looking for verbatim occurrences of

"[ :: ]" := nil

second

the key

"[ :: x1 ]" := (x1 :: [::])

have

/andP[x /eqP->] : P a && b == c

2. the sub terms whose key matches verbatim are higher order matched (i.e. up to

"[ :: x & s ]" := (x :: s)

Open a subgoal for P a && b == c. When proved apply to it the andP view, de-

deﬁnition unfolding and recursive function computation) against the pattern

"[ :: x1 , x2 , .. , xn & s ]" :=

struct the conjunction, introduce x, apply the view eqP to turn b == c into b = c,

(x1 :: x2 :: .. (xn :: s) ..)

then rewrite with it and discard the equation

3. if the matching fails, the next sub term whose key matches is tried

"[ :: x1 ; x2 ; .. ; xn ]" :=

elim: n.+1 {-2}n (ltnSn n)=> {n}// n

(x1 :: x2 :: .. [:: xn] ..)

4. if the matching succeeds, the sub term is considered to be the (only) instance of

General induction over n, note that the ﬁrst goal has a false assumption

"s1 ++ s2" := (cat s1 s2)

the pattern

n, n < 0 -> ... and is thus solved by //

forall

Notations for iterated operations

5. the sub terms selected by the pattern are then all the copies of the instance of

n : nat

the pattern

n : nat

=========

"\big [ op / idx ]_ i F" :=

=========

6. these copies are searched looking again at the key, and higher order comparing

(forall

m, m < n -> P m) ->

"\big [ op / idx ]_ ( i | P ) F" :=

P n

the arguments pairwise

forall

m, m < n.+1 -> P m

"\big [ op / idx ]_ ( i <- r | P ) F" :=

"\big [ op / idx ]_ ( m <= i < n | P ) F" :=

rewrite

lem1 ?lem2 //

Note: occurrence numbers can be combined with patterns. They refer to the list of of

"\big [ op / idx ]_ ( i < n | P ) F" :=

Use the equation with premises lem1, then get rid of the side conditions with lem2

sub terms selected by the (last) pattern (i.e. they are processed at the very end).

"\big [ op / idx ]_ ( i \in A | P ) F" :=

set

n := {2 4}(_ + b)

"\sum_ i F" :=

Put in the context a local deﬁnition named n for the second and fourth occurrences

Searching

"\prod_ i F" :=

of the sub terms selected by the pattern (_ + b)

"\max_ i F" :=

_ addn (_ * _) "C"

ssrnat

"\bigcap_ i F" :=

=========

Search for all theorems with no constraints on the main conclusion (conclusion

"\bigcup_ i F" :=

a + c + (a + b) + (a + b) =

head symbol is the wildcard _), that talk about the addn constant, matching any-

a + (a + b) + (0 + a + b) + c

caveat : in the general form, the iterated operation op is displayed in preﬁx form (not

where the pattern (_ * _) and having a name containing the string "C" in the

module ssrnat

in inﬁx form) caveat : the string "big" occurs in every lemma concerning iterated

n := a + b

operations

=========

Rewrite patterns

Misc notations

a + c + (a + b) + n =

a + (a + b) + n + c

rewrite

[pat]lem

[in

pat2]lem2 [X

pat3]lem3

Rewrite the subterms selected by the pattern pat with lem. Then in the subterms

"f1 \o f2" := (comp f1 f2)

selected by the pattern pat2 match the pattern inferred from the left hand side of

"x \in A" := (in_mem x (mem A))

lem2 and rewrite the terms selected by it. Last, in the sub terms selected by pat3

"x \notin A" := (~~ (x

\in

A))

rewrite with lem3 the sub terms identiﬁed by X exactly

"[ /\ P1 , P2 & P3 ]" := (and3 P1 P2 P3)

Idp Cheat Sheet Page 2

Related Articles

Related forms

Related Categories