Simon ! mice !^{newsflash}

-1

inductive predicates

logical verification week 5 2004 10 06

recap in abstracto

what is an inductive type?

‘minimal set such that constructors exist’

‘free’

all terms built with only constructors are different

inductive type = set of all ‘terms’

what do you get?

• a new type

      nat

• constructor functions O and S

• match + ι-reduction

      match . . . with O => . . . | S m => . . . end

• induction principle

universes

terms  ^{types}  _{kinds}_{S O}  :  _{nat} : _{Set} : _{Type} : _{Type} : _{. . .}_{fun x:A => x} : _{A -> A} : _{Prop} :

inductive types can be defined in each universe

Inductive . . . : Set :=

…

Inductive . . . : Prop :=

…

Inductive . . . : Type :=

…

inductive types for datatypes

booleans

Inductive bool : Set :=
| true : bool
| false : bool.

enumeration types

Inductive color : Set :=
| black : color
| white : color
| red : color
| yellow : color
| green : color
| blue : color
| brown : color
| orange : color
| purple : color
| pink : color
| gray : color.

singleton type

Inductive unit : Set :=
    tt : unit.

empty type

Inductive Empty_set : Set :=
    .

natural numbers

Inductive nat : Set :=
| O : nat
| S : nat -> nat.

linear lists of natural numbers

Inductive natlist : Set :=
| nil : natlist
| cons : nat -> natlist -> natlist.

polymorphic linear lists

Inductive list (A : Set) : Set :=
| nil : list A
| cons : A -> list A -> list A.

unlabeled binary trees

Inductive bintree : Set :=
| leaf : bintree
| node : bintree -> bintree -> bintree.

polymorphic labeled binary trees

Inductive bintree (A B : Set) : Set :=
| leaf : B -> bintree A B
| node : A -> bintree A B -> bintree A B -> bintree A B.

option type

Inductive option (A : Set) : Set :=
| Some : A -> option A
| None : option A.

disjoint union of two types

Inductive sum (A B : Set) : Set :=
| inl : A -> sum A B
| inr : B -> sum A B.

cartesian product of two types

Inductive prod (A B : Set) : Set :=
    pair : A -> B -> prod A B.

inductive types for logic

Curry-Howard-de Bruijn isomorphism

proposition is true ⇕ type is inhabited

truth

Inductive True : Prop :=
    I : True.

falsum

Inductive False : Prop :=
    .

conjunction

Inductive and (A B : Prop) : Prop :=
    conj : A -> B -> and A B.
Notation "A /\ B" := (and A B) : type_scope.

disjunction

Inductive or (A B : Prop) : Prop :=
| or_introl : A -> or A B
| or_intror : B -> or A B

datatypes in Set ⟷ logic in Prop

unit ⟷ True
Empty_set ⟷ False
prod ⟷ and
 sum ⟷ or

inductive predicates

Curry-Howard-de Bruijn isomorphism

predicate is true

⇕

inductive type is inhabited

even natural numbers

Inductive even : nat -> Prop :=
| even_O : even O
| even_S_S : forall n, even n -> even (S (S n)).

even and odd natural numbers

Inductive even : nat -> Prop :=
  | even_O : even O
  | even_S : forall n, odd n -> even (S n)
with odd : nat -> Prop :=
    odd_S : forall n, even n -> odd (S n).

n ≤ m

Inductive le (n:nat) : nat -> Prop :=
| le_n : le n n
| le_S : forall m:nat, le n m -> le n (S m).

sorted lists of natural numbers

Inductive Sorted : natlist -> Prop :=
| Sorted_nil : Sorted nil
| Sorted_one : forall n : nat, Sorted (cons n nil)
| Sorted_cons :
    forall (l : natlist) (n m : nat),
      Sorted (cons m l) -> le n m ->
        Sorted (cons n (cons m l)).

Leibniz equality

Inductive eq (A : Set) (x : A) : A -> Prop :=
    refl_equal : eq A x x.

coq tactics

applying the induction principle

  • elim
  • induction

inversion

Lemma not_even_1 : ~(even 1).
• inversion

what does inversion do?

abstract explanation

elimination proves universally quantified properties

∀x_{1}, …, x_{l}. I(x_{1}, …, x_{l}) ⇒ P (x_{1}, …, x_{l})

• what to do with I(t_{1}, …, t_{l}) ⇒ P (t_{1}, …, t_{l}) when t_{i} are not variables?

• generalize to ∀x_{1}, …, x_{l}. I(x_{1}, …, x_{l}) ⇒ P (x_{1}, …, x_{l})

• what to do if the generalization does not hold?

• find another one which works: ∀x_{1}, …, x_{l}. I(x_{1}, …, x_{l}) ⇒ \underbrace{(x_{1}, …, x_{l}) = (t_{1}, …, t_{l}) ⇒ P (t_{1}, …, t_{l})}

example

constructors

   even_O : even (0)  even_S_S : ∀n. even (n) ⇒ even (n + 2)

induction principe

\frac{P (0) ∀n. even (n) ⇒ P (n) ⇒ P (n + 2)}{∀n. even (n) ⇒ P (n)}

how to prove  even (1) ⇒ ⊥  ?
take:  P (n) = n = 1 ⇒ ⊥