SemProg Summary

Basics

Tactics

Some Questions that seem to be common looking at braindumps from previous years:

`contradiction`

Does contradiction solve the following goal?

Theorem x : true = false -> False.
Proof.
  intros.

No, but discriminate would.
Alternatively, inversion H or even by [].

`inversion`

What is the difference between induction and inversion?

inversion introduces a goal for each constructor of the proposition.
So does induction, but it also introduces an induction hypothesis for any inductive constructors (such as suc x).

Propositions As Types

conjunction

inductive datatype with constructor taking in two premises.

Inductive conj (A : Prop) (B : Prop) : Prop :=
  conj_intro : forall (a : A) (b : B),  conj A B.

disjunction

inductive datatype with two constructors.

Inductive disj (A : Prop) (B : Prop) : Prop :=
| inl : forall (a : A), disj A B
| inr : forall (b : B), disj A B.

existential

Inductive ex (X: Type) (P: X -> Prop) : Prop :=
  ex_intro : forall (x : X), P x -> ex X P.

Induction Principles

Other

functional extensionality

Axiom func_ext : forall x, f x = g x -> f = g.

Hoare Rules

A Hoare Triple \(\{P\}\ \mathrm{c}\ \{Q\}\) consists of Assertions \(P\), \(Q\) and a command c.
If c is started in a state satisfying \(P\), and if c terminates! in some final state, then \(Q\) will hold for the final state.

Rules

`hoare_skip`

Theorem hoare_skip : forall P,
    {{P}} SKIP {{P}}.

`hoare_asgn`

Theorem hoare_asgn : forall Q X a,
  {{Q [X |--> a]}} (X := a) {{Q}}.

`hoare_seq`

Theorem hoare_seq : forall P Q R c1 c2,
    {{Q}} c2 {{R}} ->
    {{P}} c1 {{Q}} ->
    {{P}} c1;c2 {{R}}.

`hoare_if`

Theorem hoare_if : forall P Q (b:bexp) c1 c2,
  {{ P /\ b }} c1 {{Q}} ->
  {{ P /\ ~ b}} c2 {{Q}} ->
  {{P}} (IF b THEN c1 ELSE c2 END) {{Q}}.

`hoare_while`

Theorem hoare_while : forall P (b:bexp) c,
  {{P /\ b}} c {{P}} ->
  {{P}} WHILE b DO c END {{P /\ ~ b}}.

Decorated Programs

Definition swap (m n : nat) : decorated :=
    <{  {{ X = m /\ Y = n}} ->>
        {{ (X + Y) - ((X + Y) - Y) = n /\ (X + Y) - Y = m }}
    X := X + Y
        {{ X - (X - Y) = n /\ X - Y = m }};
    Y := X - Y
        {{ X - Y = n /\ Y = m }};
    X := X - Y
        {{ X = n /\ Y = m}} }>.

STLC

Concepts

Values

Inductive value : tm -> Prop :=
  | v_abs : forall x T2 t1,
      value <{\x:T2, t1}>
  | v_true :
      value <{true}>
  | v_false :
      value <{false}>.

stuckness

Definition stuck (t:tm) : Prop :=
  stlc_normal_form t /\ ~ value t.

Operational Semantics

small-step

Inductive step : tm -> tm -> Prop :=
| ST_AppAbs : forall x T2 t1 v2,
    value v2 ->
    <{(\x:T2, t1) v2}> --> <{ [x:=v2]t1 }>
| ST_App1 : forall t1 t1' t2,
    t1 --> t1' ->
    <{t1 t2}> --> <{t1' t2}>
| ST_App2 : forall v1 t2 t2',
    value v1 ->
    t2 --> t2' ->
    <{v1 t2}> --> <{v1  t2'}>
| ST_IfTrue : forall t1 t2,
    <{if true then t1 else t2}> --> t1
| ST_IfFalse : forall t1 t2,
    <{if false then t1 else t2}> --> t2
| ST_If : forall t1 t1' t2 t3,
    t1 --> t1' ->
    <{if t1 then t2 else t3}> --> <{if t1' then t2 else t3}>

where "t '-->' t'" := (step t t').

big-step

Typing

Inductive has_type : context -> tm -> ty -> Prop :=
    | T_Var : forall Gamma x T1,
      Gamma x = Some T1 ->
      Gamma |-- x :-> T1
    | T_Abs : forall Gamma x T1 T2 t1,
      Gamma,, x :-> T2 |-- t1 :-> T1 ->
      Gamma |-- \x:T2, t1 :-> (T2 -> T1)
    | T_App : forall T1 T2 Gamma t1 t2,
      Gamma |-- t1 :-> (T2 -> T1) ->
      Gamma |-- t2 :-> T2 ->
      Gamma |-- t1 t2 :-> T1
    | T_True : forall Gamma,
      Gamma |-- true :-> Bool
    | T_False : forall Gamma,
      Gamma |-- false :-> Bool
    | T_If : forall t1 t2 t3 T1 Gamma,
      Gamma |-- t1 :-> Bool ->
      Gamma |-- t2 :-> T1 ->
      Gamma |-- t3 :-> T1 ->
      Gamma |-- if t1 then t2 else t3 :-> T1

Theorems

progress theorem

Closed, well-typed terms are not stuck.

Theorem progress : forall t T,
  ## |-- t :-> T ->
  value t \/ exists t', t --> t'.

substitution lemma

Substituting a closed term v for a variable x in a term t preserves the type of t.

Lemma substitution_preserves_typing : forall Gamma x U t v T,
     Gamma,, x :-> U |-- t :-> T ->
     ## |-- v :-> U   ->
     Gamma |-- [x:=v]t :-> T.

weakening lemma

Typing is preserved when the context is expanded.

Lemma weakening : forall Gamma Gamma' t T,
     (forall x Tx, Gamma x = Some Tx -> Gamma' x = Some Tx) ->
     Gamma |-- t :-> T  ->
     Gamma' |-- t :-> T.

preservation theorem

If a closed term t has type T and takes a step to t', then t' is also a closed term with Type T.

Theorem preservation : forall t t' T,
  ## |-- t :-> T  ->
  t --> t'  ->
  ## |-- t' :-> T.

soundness

A well typed term can never reach a stuck state.

Corollary soundness : forall t t' T,
  ## |-- t :-> T ->
  t -->* t' ->
  ~(stuck t').