gistfile1.coq

Require Import String.
Require Import List.
Require Import Compare_dec.

Record user :=
  { name : string
  ; age : nat
  }
.

Inductive schlemazl :=
| Loh
| Mudak
| Pots
.

Axiom action : Type.
Axiom deactivate : user -> action.

Definition ban_user (u : user) : (schlemazl * list action) :=
  let actions := deactivate u :: nil in
  let res :=
    if lt_dec u.(age) 10
    then Loh
    else
    if lt_dec u.(age) 20
    then Mudak
    else Pots
  in
    (res, actions)
.

Lemma ban_user_8 :
  forall name,
    let u := {| name := name; age := 8 |} in
    exists actions,
    ban_user u = (Loh, actions).

intros.
compute.
eauto.

Defined.