Spahn Gallina example

The expression

match term0 return_type with pattern1 => term1 | … | patternn => termn end

denotes a pattern-matching over the term term0 (expected to be of an inductive type I). The terms term1…termn are the branches of the pattern-matching expression. Each of patterni has a form qualid ident … ident where qualid must denote a constructor. There should be exactly one branch for every constructor of I.

Coq < Inductive bool : Type := true : bool | false : bool.

{}

Coq < Inductive eq (A:Type) (x:A) : A -> Prop := eq_refl : eq A x x.

{}

Coq < Inductive or (A:Prop) (B:Prop) : Prop :=

Coq < | or_introl : A -> or A B

Coq < | or_intror : B -> or A B.

{}

Coq < Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false)

Coq < := match b as x return or (eq bool x true) (eq bool x false) with

Coq < | true => or_introl (eq bool true true) (eq bool true false)

Coq < (eq_refl bool true)

Coq < | false => or_intror (eq bool false true) (eq bool false false)

Coq < (eq_refl bool false)

Coq < end.