SSReflectCheatSheet

SSReflectCheatSheet

SSReflect CheatSheet

移転中 => http://kikwiki.wikkii.com/wiki/SSReflect_CheatSheet

ここから下は古い

Import

Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq.
Require Import paths choice fintype tuple finset.

Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.

Definitions

Basic tactics

名前意味
moveIntroduction/Dischargeだけをしたいときに使う
caseスタックの先頭で場合わけ
elimスタックの先頭で帰納法
applyスタックの先頭をapply
exact

Discharge

':'で指定する。':'の後ろに書いたものを右のからスタックにつんでいく。ゴールにつながってるproduct termのことをスタックに見立てる。

記法意味
move: x G ==> forall x, G。LCからxを消す
move: H G ==> P -> G。LCからHを消す
move: x y z H H0 H1 G ==> forall x y z, P -> P0 -> P1 -> G。LCから略を消す
move: {2}x G x x x ==> forall x0, G x x0 x
move: {-2}x G x x x ==> forall x0, G x0 x x0
move: (refl_equal n) G ==> n = n -> G
move: (x)move: xと同じ。ただしxを消さない
move: {+}x同上

moveのほかにcase, elim, apply, exact, "view tactical"を使用可能。一番左の項に対してそのtacticを適用する。

':'の前に<ident>を置くと、等式を生成する

記法意味
move En: (size l) => nG (size l) ==> G n。LCにEn: (size l) = nを加える
case E: a => [|n]G a ==> G OとG (S n)。LCにE: a = OとE: a = S nを加える

case/elimの場合にmatch ... in ... return ... のところを指定できるような機能

記法意味
case {1 3}l / (lastP l)TBD

Introduction

'=>'で指定する。'=>'の後ろに書いた名前で左のからスタックをポップしていく。

記法意味
move=> xforall x, G ==> G。LCにxを加える
move=> HP->G ==> G。LCにHを加える
move=> ?同上。ただし名前を勝手に決める
move=> _同上。ただしLCに加えない
move=> *残ってるproductを全部ポップする
move=> ->x=y -> G x y ==> G y y
move=> <-x=y -> G x y ==> G x x
move=> [x|y]場合わけ。intro patternと同様
move=> //try done. と同じ
move=> /=simpl. と同じ
move=> //=上二つを続けて
move=> {IHn}////と同じ。ただしIHnを使おうとする。IHnをLCから消す

moveのほかに好きなtacticを使用可能。最初にそれを実行してからIntroductionを行う。

Control flow

TBD

Rewriting

  • 単なる置き換えだけじゃなくて、simpl, fold, unfold, closing of goalsなんかができる。
  • 複数の置き換えを一個のrewriteに並べて書ける
  • 書き換え位置の指定が便利になった

prefix

各書き換えの前に置ける

反転

記法意味
-<-と->を反転。unfoldfoldを反転

回数指定

記法意味
3!E3回繰り返す
!1回以上繰り返す
?0回以上繰り返す
3?0-3回繰り返す

位置指定

記法意味
{2}2番目
{-2}2番目以外
[f x _]f x _ にマッチした箇所
{2}[f x _]2番目にマッチした箇所

書き換え

記法意味
//try done
/=simpl
//=simpl; try done
/nameunfold name
termrewrite term
(term, term, ..., term)同じプリフィックスで複数実行
(_: term)cutrewrite term

特別な場合

記法意味
rewrite -[foo x]/barchange (foo x) with bar

Locking, unlocking

記法意味
rewrite {2}[cons]locksimplされないように2番目のconsをロック
rewrite -unlock全部アンロック
unlock {2}f2番目のfをアンロック
記法意味
Notation "'nosimpl' t"tをsimplから保護する。unfoldで解除

Congruence

記法意味
congr f f x y z = f a b c ==> x = a, y = b, z = c
congr 2 f引数の数を制限
congr (_ + (_ * _))congr (fun x y z => x + (y * z))と同じ

View and reflection

elim/V

記法意味
elim/V: xelim x using V
elim/V E: xさらに=を生成

assumption

記法意味
move/V: x => yxをVに適用
case/V: x => [y z]適用したあとに場合わけ
move/(_ x)specializeに使える

view hintに入ってる変換を自動で行ってくれる(iffLRなど)

goal

記法意味
apply/Vview hintを使いつつapply

reflect

記法意味
apply/norP/idP?

Searching tool

Using th libraries



Notation

let:

let: <pattern> := <term>1 in <term>2.
let: <pattern>1 as <ident> in <pattern>2 := <term>1 return <term>2 in <term>3.

if then else

if <term>1 is <pattern>1 then <term>2 else <term>3.
if <term>1 is <pattern>1 as <ident> in <pattern>2 return <term>2 then <term>3 else <term>4.

Anonymous arguments

Inductive list (A : Type) : Type := nil | cons of A & list A.

theorem

command

Structure/Contextual Implicits

Search

guideline

suffixes

以下メモ

ssreflect/theoriesの中をさらっと読んで、

  • イミフなtacticがあったらここにメモ
  • よく使いそうな定数があったらここにメモ
  • よく使いそうな記法があったらry

zmodp.v

Definition Zp : {set 'I_p} := setT.
Implicit Types x y z : 'I_p.
Definition inZp i := Ordinal (ltn_pmod i p_gt0).
rewrite modn_small ?ltn_ord.
apply: val_inj;
rewrite /= modZp.
inZp 1
predArgType
ZpUnit x of coprime p x.
Coercion Zp_unit_val u := let: ZpUnit x _ := u in x.
Canonical Structure Zp_unit_subType :=
  Eval hnf in [subType for Zp_unit_val by Zp_unit_rect].
exact: valZpK.
apply/centsP=> x _ y _;

prime.v

if n is 0 then y else x.
    if (b == 0) && (c == 0) then
let: (e2, m2) := elogn2 0 n.-1 n.-1 in
  let pd_val pd := \prod_(f <- pd) pfactor f.1 f.2 in 
  let lb_dvd q m := ~~ has [pred d | d %| m] (index_iota 2 q) in
case: prime_decomp => [|[q [|[|e]]] pd] //=; last first; last by rewrite andbF.
  rewrite {1}/pfactor 2!expnS -!mulnA /=.
  case: (_ ^ _ * _) => [|u -> _]; first by rewrite !muln0.
  case/andP=> lt1q _; left; right; exists q; last by rewrite dvdn_mulr.
Lemma mem_primes : forall p n,
  (p \in primes n) = [&& prime p, n > 0 & p %| n].
move=> n; case: (posnP n) => [-> // | ]; case/prime_decomp_correct=> _ _.


ちゃんと理解したら下に書く

move=> m n le_mn

はほげほげ。