Require Import Arith.


Section Domain.

Variable Dom : Set.

Inductive tree : Set :=
  | leaf : Dom → tree
  | cons : tree → tree → tree.

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 t2 ⇒ leavemult 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 t2 ⇒ Has_Zero t1 ∨ Has_Zero t2
  end.


Lemma zero_occ : ∀ t : nat_tree, Has_Zero t → leavemult 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 t → SPECIF 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' t → kappa 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.