proposition: Lemma interp_unicity : forall t, Acc interp_call t -> forall s1 s2, Interp t s1 -> Interp t s2 -> s1 = s2.
proof: Proof. intros t Acc_t; induction Acc_t as [t Acc_t IH]. destruct t as [x | f l]; intros s1 s2 H1 H2; inversion H1 as [ | f1 l1 l1' ll1 Cf1 Hl1 Hl1' Hll1 | f1 l1 l1' ll1 k1 kk1 Df1 Hl1 Hl1' Hll1 Hk1 Hk1' Hkk1]; inversion H2 as [ | f2 l2 l2' ll2 Cf2 Hl2 Hl2' Hll2 | f2 l2 l2' ll2 k2 kk2 Df2 Hl2 Hl2' Hll2 Hk2 Hk2' Hkk2]; subst; trivial. do 2 apply f_equal. assert (K : forall s s1 s2, In (s,s1) ll1 -> In (s,s2) ll2 -> s1 = s2). intros s s1 s2 ss1_in_ll1 ss2_in_ll2. assert (s_in_l : In s (map (fun st => fst st) ll1)). rewrite in_map_iff; exists (s,s1); split; trivial. apply IH with s. left; assumption. destruct (in_split _ _ s_in_l) as [kk1 [kk2 K]]. apply Hll1; assumption. apply Hll2; assumption. clear -Hl2 K. revert ll2 Hl2 K. induction ll1 as [ | [s s1] ll1]; intros [ | [s' s2] ll2] Hl2 K; trivial. discriminate. discriminate. simpl in Hl2; injection Hl2; clear Hl2; intros H' s_eq_s'; subst s'. rewrite (K s s1 s2); try (left; trivial). rewrite IHll1 with ll2; trivial. intros t t1 t2 tt1_in_ll1 tt2_in_ll2; apply (K t t1 t2); right; trivial. absurd (G f); trivial. absurd (G f); trivial. apply f_equal; apply f_equal2. do 2 apply f_equal. assert (K : forall s s1 s2, In (s,s1) ll1 -> In (s,s2) ll2 -> s1 = s2). intros s s1 s2 ss1_in_ll1 ss2_in_ll2. assert (s_in_l : In s (map (fun st => fst st) ll1)). rewrite in_map_iff; exists (s,s1); split; trivial. apply IH with s. left; assumption. destruct (in_split _ _ s_in_l) as [lll1 [lll2 K]]. apply Hll1; assumption. apply Hll2; assumption. clear -Hl2 K. revert ll2 Hl2 K. induction ll1 as [ | [s s1] ll1]; intros [ | [s' s2] ll2] Hl2 K; trivial. discriminate. discriminate. simpl in Hl2; injection Hl2; clear Hl2; intros H' s_eq_s'; subst s'. rewrite (K s s1 s2); try (left; trivial). rewrite IHll1 with ll2; trivial. intros t t1 t2 tt1_in_ll1 tt2_in_ll2; apply (K t t1 t2); right; trivial. apply f_equal. assert (K : forall s s1 s2, In (s,s1) kk1 -> In (s,s2) kk2 -> s1 = s2). intros s s1 s2 ss1_in_kk1 ss2_in_kk2. assert (s_in_l : In s (map (fun st => fst st) kk1)). rewrite in_map_iff; exists (s,s1); split; trivial. apply IH with s. right; trivial. rewrite <- FB; rewrite Hk1; assumption. destruct (in_split _ _ s_in_l) as [kkk1 [kkk2 K]]. apply Hkk1; assumption. apply Hkk2; assumption. rewrite Hk1 in Hk2. clear -Hk2 K. revert kk2 Hk2 K. induction kk1 as [ | [s s1] kk1]; intros [ | [s' s2] kk2] Hk2 K; trivial. discriminate. discriminate. simpl in Hk2; injection Hk2; clear Hk2; intros H' s_eq_s'; subst s'. rewrite (K s s1 s2); try (left; trivial). rewrite IHkk1 with kk2; trivial. intros t t1 t2 tt1_in_ll1 tt2_in_ll2; apply (K t t1 t2); right; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp graph_dp terminaison interp)