# Views using dependent pattern-matching

The user can write a view function to implement this. First one needs to write
a discriminator for the inductive type, indicating which cases are to be merged together:

One can derive an inductive representing the view of three as cone and the two other
ctwo and cthree cases lumbed together.

Inductive three_two_view : three → Set :=

| three_one : three_two_view cone

| three_other c : discr_three c → three_two_view c.

| three_one : three_two_view cone

| three_other c : discr_three c → three_two_view c.

This view is obviously inhabited for any element in three.

Equations three_viewc c : three_two_view c :=

three_viewc cone := three_one;

three_viewc c := three_other c I.

three_viewc cone := three_one;

three_viewc c := three_other c I.

Using a with clause one can pattern-match on the view argument to
do case splitting on three using only two cases. In each branch,
one can see that the three variable is determined by the view pattern.

Equations onthree (c : three) : three :=

onthree c with three_viewc c :=

onthree ?(cone) three_one := cone;

onthree ?(c) (three_other c Hc) := c.

onthree c with three_viewc c :=

onthree ?(cone) three_one := cone;

onthree ?(c) (three_other c Hc) := c.

A similar example discriminating 10 from the rest of natural numbers.

First alternative: using an inductive view

Module View.

Inductive view_discr_10 : nat → Set :=

| view_discr_10_10 : view_discr_10 10

| view_discr_10_other c : discr_10 c → view_discr_10 c.

This view is obviously inhabited for any element in three.

Equations discr_10_view c : view_discr_10 c :=

discr_10_view 10 := view_discr_10_10;

discr_10_view c := view_discr_10_other c I.

Equations f (n:nat) : nat :=

f n with discr_10_view n :=

f ?(10) view_discr_10_10 := 0;

f ?(n) (view_discr_10_other n Hn) := n + 1.

Goal ∀ n, n ≠ 10 → f n = n + 1.

intros n; apply f_elim.

(* 2 cases: 10 and not 10 *)

all:simpl; congruence.

Qed.

End View.

discr_10_view 10 := view_discr_10_10;

discr_10_view c := view_discr_10_other c I.

Equations f (n:nat) : nat :=

f n with discr_10_view n :=

f ?(10) view_discr_10_10 := 0;

f ?(n) (view_discr_10_other n Hn) := n + 1.

Goal ∀ n, n ≠ 10 → f n = n + 1.

intros n; apply f_elim.

(* 2 cases: 10 and not 10 *)

all:simpl; congruence.

Qed.

End View.

Second alternative: using the discriminator directly.
This currently requires massaging the eliminator a bit

Equations f (n:nat) : nat by struct n (* FIXME *) :=

{ f 10 := 0;

f x := brx x (I : discr_10 x) }

where brx (x : nat) (H : discr_10 x) : nat :=

brx x H := x + 1.

Lemma f_elim' : ∀ (P : nat → nat → Prop),

P 10 0 →

(∀ (x : nat) (H : discr_10 x), P x (x + 1)) →

(∀ n : nat, P n (f n)).

Proof.

intros. apply (f_elim P (fun x H r ⇒ P x r)); auto.

Defined.

Goal ∀ n, n ≠ 10 → f n = n + 1.

intros n; apply f_elim'.

(* 2 cases: 10 and not 10 *)

all:simpl; congruence.

Qed.

This page has been generated by coqdoc