# Library Exceptions.leavemult

Require Import Arith.

Section Domain.

Variable Dom : Set.

Inductive tree : Set :=
| leaf : Domtree
| cons : treetreetree.

End Domain.

Definition nat_tree := tree nat.
Definition nat_cons := cons nat.
Definition nat_leaf := leaf nat.

Fixpoint leavemult (t : nat_tree) : nat :=
match t return nat with
| leaf n1
n1

| cons t1 t2leavemult t1 × leavemult t2
end.

Definition SPECIF (t : nat_tree) := {n : nat | n = leavemult t}.

Theorem trivialalgo : t : nat_tree, SPECIF t.

intro t.
unfold SPECIF in |- ×.
apply exist with (leavemult t); auto with v62.
Defined.

Fixpoint Has_Zero (t : nat_tree) : Prop :=
match t return Prop with
| leaf n1
n1 = 0

| cons t1 t2Has_Zero t1 Has_Zero t2
end.

Lemma zero_occ : t : nat_tree, Has_Zero tleavemult t = 0.

simple induction t.
simple induction d; simpl in |- *; auto with v62. intros t1 H1 t2 H2 H.
simpl in |- ×. elim H; intro H0.
cut (leavemult t1 = 0). intro H3. rewrite H3; simpl in |- *; auto with v62. auto with v62.
cut (leavemult t2 = 0). intro H3. rewrite H3; simpl in |- ×.
symmetry in |- *; apply mult_n_O. auto with v62.
Qed.

Let subtree_ersatz (t' t : nat_tree) := Has_Zero t'Has_Zero t.

Let kappa (t t' : nat_tree) := n' : nat, n' = leavemult t'SPECIF t.

Theorem cpsalgo : t : nat_tree, SPECIF t.

intro.
cut (Has_Zero tSPECIF t).
intro ESCAPE_O.

2: intro.
2: unfold SPECIF in |- ×.
2: apply exist with 0.
2: symmetry in |- ×.
2: apply zero_occ.
2: auto with v62.

Hint Unfold subtree_ersatz: v62.
Hint Unfold kappa: v62.

cut ( t' : nat_tree, subtree_ersatz t' tkappa t t'SPECIF t).
Hint Unfold SPECIF: v62.

intro AUX.
apply AUX with t.
auto with v62.
unfold kappa in |- ×.
intros n H.
unfold SPECIF in |- *; apply exist with n; auto with v62.

simple induction t'.
simple induction d.
intros H H0.
apply ESCAPE_O.
apply H. simpl in |- ×.
auto with v62.
intros y H1 H2 H3.
unfold kappa in H3.
apply H3 with (S y).
simpl in |- ×.
auto with v62.

intro t1. intro ind1. intro t2. intro ind2. intros H H0.
apply ind2.
intro H1.
apply H.
unfold Has_Zero in |- ×.
unfold Has_Zero in H1. auto with v62.

unfold kappa in |- ×.
unfold kappa in H0.
intros n2 eg2.

apply ind1.
intro.
apply H.
simpl in |- *; auto with v62.
unfold kappa in |- ×.
intros n1 eg1.
apply H0 with (n1 × n2).
simpl in |- ×.
rewrite eg2; rewrite eg1.
auto with v62.

Defined.

Extraction "leavemult.ml" SPECIF kappa trivialalgo cpsalgo.