#+title: SemProg Summary
#+author: Florian Guthmann
#+email: florian.guthmann@fau.de
#+options: toc:nil num:nil \n:t html-style:nil html5-fancy:t
#+html_doctype: xhtml5

#+html_head: <link rel="stylesheet" type="text/css" href="/~oc45ujef/style/org.css"/>
* Basics
** Tactics
Some Questions that seem to be common looking at [[https://fsi.cs.fau.de/dw/pruefungen/hauptstudium/ls8][braindumps]] from previous years:
*** ~contradiction~
Does ~contradiction~ solve the following goal?
#+begin_src coq
  Theorem x : true = false -> False.
  Proof.
    intros.
#+end_src
No, but ~discriminate~ would.
Alternatively, ~inversion H~ or even ~by []~.
*** ~inversion~
:PROPERTIES:
:CUSTOM_ID: inversion
:END:
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.
#+begin_src coq
Inductive conj (A : Prop) (B : Prop) : Prop :=
  conj_intro : forall (a : A) (b : B),  conj A B.
#+end_src
*** disjunction
inductive datatype with two constructors.
#+begin_src coq
Inductive disj (A : Prop) (B : Prop) : Prop :=
| inl : forall (a : A), disj A B
| inr : forall (b : B), disj A B.
#+end_src
*** existential
#+begin_src coq
Inductive ex (X: Type) (P: X -> Prop) : Prop :=
  ex_intro : forall (x : X), P x -> ex X P.
#+end_src
** Induction Principles
# TODO

** Other
*** functional extensionality
#+begin_src coq
Axiom func_ext : forall x, f x = g x -> f = g.
#+end_src

* 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~
#+begin_src coq
Theorem hoare_skip : forall P,
    {{P}} SKIP {{P}}.
#+end_src

*** ~hoare_asgn~
#+begin_src coq
Theorem hoare_asgn : forall Q X a,
  {{Q [X |--> a]}} (X := a) {{Q}}.
#+end_src

*** ~hoare_seq~
#+begin_src coq
Theorem hoare_seq : forall P Q R c1 c2,
    {{Q}} c2 {{R}} ->
    {{P}} c1 {{Q}} ->
    {{P}} c1;c2 {{R}}.
#+end_src

*** ~hoare_if~
#+begin_src coq
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}}.
#+end_src

*** ~hoare_while~
#+begin_src coq
Theorem hoare_while : forall P (b:bexp) c,
  {{P /\ b}} c {{P}} ->
  {{P}} WHILE b DO c END {{P /\ ~ b}}.
#+end_src

** Decorated Programs
#+begin_src coq
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}} }>.
#+end_src

* STLC

** Concepts

*** Values
#+begin_src coq
Inductive value : tm -> Prop :=
  | v_abs : forall x T2 t1,
      value <{\x:T2, t1}>
  | v_true :
      value <{true}>
  | v_false :
      value <{false}>.
#+end_src

*** stuckness
#+begin_src coq
Definition stuck (t:tm) : Prop :=
  stlc_normal_form t /\ ~ value t.
#+end_src

** Operational Semantics

*** small-step
#+begin_src coq
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').
#+end_src

*** big-step

** Typing
#+begin_src coq
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
#+end_src

** Theorems

*** progress theorem
Closed, well-typed terms are not stuck.
#+begin_src coq
Theorem progress : forall t T,
  ## |-- t :-> T ->
  value t \/ exists t', t --> t'.
#+end_src

*** substitution lemma
Substituting a *closed* term ~v~ for a variable ~x~ in a term ~t~ preserves the type of ~t~.
#+begin_src coq
Lemma substitution_preserves_typing : forall Gamma x U t v T,
     Gamma,, x :-> U |-- t :-> T ->
     ## |-- v :-> U   ->
     Gamma |-- [x:=v]t :-> T.
#+end_src

*** weakening lemma
Typing is preserved when the context is expanded.
#+begin_src coq
Lemma weakening : forall Gamma Gamma' t T,
     (forall x Tx, Gamma x = Some Tx -> Gamma' x = Some Tx) ->
     Gamma |-- t :-> T  ->
     Gamma' |-- t :-> T.
#+end_src

*** 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~.
#+begin_src coq
Theorem preservation : forall t t' T,
  ## |-- t :-> T  ->
  t --> t'  ->
  ## |-- t' :-> T.
#+end_src

*** soundness
A well typed term can *never* reach a stuck state.
#+begin_src coq
Corollary soundness : forall t t' T,
  ## |-- t :-> T ->
  t -->* t' ->
  ~(stuck t').
#+end_src