proposition: Lemma tree_value_injective t1 t2: treep t1 -> treep t2 -> (forall E, slist_good (tree_size t1) (tree_size t2) E -> tree_value E t1 = tree_value E t2) -> t1 = t2.
proof: Proof. move => ha hb hc. move: (Tree_to_tree_surjective ha) => [e ev]. move: (Tree_to_tree_surjective hb) => [e' ev']. rewrite ev ev'; f_equal. have: forall E, slist_good (nat_to_B (Tsize e)) (nat_to_B (Tsize e')) E -> Tree_value E e = Tree_value E e'. move => E; move: (hc E); rewrite ev ev'. move:(Tree_to_tree_prop e) =>[_ _ -> _]. move:(Tree_to_tree_prop e') =>[_ _ -> _]. rewrite !Tree_value_compat //. clear. have Ne1: nonempty \1c by exists \0c; apply:set1_1. move:clt_3 => [lt03 /proj2 ne13 _]. have Ne3: nonempty \3c by exists \0c; apply/(NltP NS3). have H0 n n' f: let m := (nat_to_B n) in let m' := (nat_to_B n') in let k := csucc (cmax m m') in let E := Lg k f in (forall i, i <c k -> (f i) = \1c \/ (f i) =\3c ) -> [/\ slist_good m m' E, Vg E m = f m & Vg E m' = f m']. simpl. move: (nat_to_B_Nat n) (nat_to_B_Nat n'). set m := nat_to_B n; set m' := nat_to_B n' => mN m'N fp. move: (Nmax_p1 mN m'N); set k := cmax _ _; move => [kN le1 le2]. have skN := NS_succ kN. have lt1: m <c csucc k by apply/(cltSleP kN). have lt1': m' <c csucc k by apply/(cltSleP kN). have p3: inc m (csucc k) by apply/(NltP skN). have p4: inc m' (csucc k) by apply/(NltP skN). have p5:slistp (Lg (csucc k) f) by split; aww. rewrite /slist_good /slength Lgd !LgV//; split => //; split => // i iln. move/(NltP skN):(iln) => iin; rewrite (LgV iin); exact: (fp _ iln). have HA n t: (forall E, slist_good (nat_to_B n) (nat_to_B (Tsize (Tpowerset t))) E -> Tree_value E (Tbase n) = Tree_value E (Tpowerset t)) -> False. move => H. set k := csucc (cmax (nat_to_B n) (nat_to_B (Tsize t))). have fp:(forall i, i <c k -> \3c = \1c \/ \3c = \3c) by move => _ _;right. move: (H0 n (Tsize (Tpowerset t)) _ fp) => [ra rb rc]. by move:(H _ ra); rewrite /= rb => /not_a_powerset3. have HB n t t': (forall E, slist_good (nat_to_B n) (nat_to_B (Tsize (Tproduct t t'))) E -> Tree_value E (Tbase n) = Tree_value E (Tproduct t t')) -> False. move => H. set k:=csucc (cmax (nat_to_B n) (nat_to_B (maxn (Tsize t) (Tsize t')))). have fp:(forall i, i <c k -> \1c = \1c \/ \1c = \3c) by move => _ _;left. move:(H0 n (Tsize (Tproduct t t')) _ fp) => [sa sb sc]. by move: (H _ sa); rewrite /= sb => /not_a_product1. have HC t t' t'' : (forall E, slist_good (nat_to_B (Tsize (Tpowerset t))) (nat_to_B (Tsize (Tproduct t' t''))) E -> Tree_value E (Tpowerset t) = Tree_value E (Tproduct t' t'')) -> False. set n := Tsize _; set n' := Tsize _ => H. set k := csucc (cmax (nat_to_B n) (nat_to_B n')). have fp:(forall i, i <c k -> \1c = \1c \/ \1c = \3c) by move => _ _;left. by move:(H0 n n' _ fp) => [/H /powerset_not_product]. have He n m E x: (slist_good n m E) -> nat_to_B (Tsize x) <c slength E -> nonempty (Tree_value E x). move => ha hb; move:(Tree_to_tree_prop x) => [ra _ rb _]. rewrite - rb in hb; rewrite - Tree_value_compat; apply: (tree_val_ne _ ra hb). by move => i ile; case: (proj33 ha _ ile) => ->. have Hf T E E': (forall i, i<=c (nat_to_B (Tsize T)) -> Vg E i = Vg E' i) -> Tree_value E T = Tree_value E' T. move => hi; rewrite - 2!Tree_value_compat. move:(Tree_to_tree_prop T) => [ra _ rb _]. by apply: (tree_value_extent ra); rewrite rb. pose ext E a b := Lg (csucc (cmax a b)) (fun z => Yo (z <c (slength E)) (Vg E z) \1c). have ext_p1 n m a b E: let E' := (ext E a b) in slist_good n m E -> natp a -> natp b -> slength E <=c csucc(cmax a b) -> [/\ slist_good a b E', a <c slength E', b <c slength E' & forall i, i <c (slength E) -> Vg E i = Vg E' i]. move => E' [ha hb hc] aN bN hd. move:(Nmax_p1 aN bN) => [ma mb mc]. set k := (csucc (cmax a b)). have le: slength (ext E a b) = k by rewrite /slength /ext; aw. have sa1: a <c slength (ext E a b) by rewrite le; apply/(cltSleP ma). have sb1: b <c slength (ext E a b) by rewrite le; apply/(cltSleP ma). have lex: slistp (ext E a b) by rewrite /slistp/ext; aw; split;fprops. have he:slist_good a b (ext E a b). split => //. rewrite le => i il. have ii:inc i k by apply /(NltP (NS_succ ma)). rewrite /ext LgV//; Ytac hi;[ by apply:hc | by left ]. split => // i il. have ii:inc i (slength E) by apply /(NltP (proj2 ha)). have ii2:inc i k by apply /(NltP (NS_succ ma)); exact:(clt_leT il hd). by rewrite /E'/ext LgV//; Ytac0; done. have mc n m: cmax (nat_to_B n) (nat_to_B m) = cmax (nat_to_B m) (nat_to_B n). by rewrite - ! nat_to_B_max maxnC. elim: e e'. - move => n e. case:e. + move => n' H. set m := (nat_to_B n). case: (equal_or_not (nat_to_B n') m) => mm. by rewrite (nat_to_B_injective mm). set k := csucc (cmax (nat_to_B n) (nat_to_B n')). have hf:(forall i, i <c k -> variant m \1c \3c i = \1c \/ variant m \1c \3c i = \3c). by move => i _; rewrite/variant; Ytac w; [left | right]. move: (H0 n n' _ hf) => [/H sa sb sc]. move: sa; rewrite /= sb sc. by rewrite (variant_true _ _ (erefl _ )) (variant_false _ _ mm) => /ne13. + move => t h; case: (HA n t h). + move => t t' h; case: (HB n t t' h). - move => t h; case. + move => n /= h1; case: (HA n t) => E [ ea eb ec]; rewrite /= h1 //. by move: eb; rewrite /= mc => eb. + move => t' /= ha; rewrite (h t') // => E ev. exact:(powerset_injective (ha _ ev)). + move => t' t'' h1; case:(HC _ _ _ h1). - move => t ht t' ht'; case. + move => n H; case: (HB n t t') => E [ea eb ec]. by rewrite mc in eb; rewrite H. + move => t'' h; case: (HC t'' t t') => E [ea eb ec]. by rewrite mc in eb; rewrite h. + move => t2 t3 /=. set l1 := maxn _ _; set l2 := maxn _ _; set l3 := maxn l1 l2 => h. move: (nat_to_B_Nat l1)(nat_to_B_Nat l2) => l1N l2N. have ->: t = t2. apply: ht => E ep. move: (ep) => [p0 p1 p2]. have se: slength E <=c csucc (cmax (nat_to_B l1) (nat_to_B l2)). rewrite p1; apply /cleSS; rewrite /l1 /l2 - 2!nat_to_B_max maxnACA. by apply/nat_to_B_le; apply: leq_maxl. have se2: nat_to_B (Tsize t) <c slength E. rewrite p1 -nat_to_B_max nat_to_B_succ; apply/nat_to_B_lt. by rewrite ltnS leq_maxl. have se3: nat_to_B (Tsize t2) <c slength E. rewrite p1 -nat_to_B_max nat_to_B_succ; apply/nat_to_B_lt. by rewrite ltnS leq_maxr. move: (ext_p1 _ _ _ _ _ ep l1N l2N se). set E' := ext _ _ _; move => [sa sb sc sd]. have pa:forall i, i <=c nat_to_B (Tsize t) -> Vg E i = Vg E' i. by move => i lin; apply: sd; exact:(cle_ltT lin se2). have pb:forall i, i <=c nat_to_B (Tsize t2) -> Vg E i = Vg E' i. move => i lin; apply: sd; exact:(cle_ltT lin se3). move: (product_injective (He _ _ _ (Tproduct t2 t3) sa sc) (h _ sa)). by rewrite -/(Tree_value _) (Hf t E E' pa) (Hf t2 E E' pb); case. have -> //: t' = t3. apply: ht' => E ep. move: (ep) => [p0 p1 p2]. have se: slength E <=c csucc (cmax (nat_to_B l1) (nat_to_B l2)). rewrite p1; apply /cleSS; rewrite /l1 /l2 - 2!nat_to_B_max maxnACA. by apply/nat_to_B_le; apply: leq_maxr. have se2: nat_to_B (Tsize t') <c slength E. rewrite p1 -nat_to_B_max nat_to_B_succ; apply/nat_to_B_lt. by rewrite ltnS leq_maxl. have se3: nat_to_B (Tsize t3) <c slength E. rewrite p1 -nat_to_B_max nat_to_B_succ; apply/nat_to_B_lt. by rewrite ltnS leq_maxr. move: (ext_p1 _ _ _ _ _ ep l1N l2N se). set E' := ext _ _ _; move => [sa sb sc sd]. have pa:forall i, i <=c nat_to_B (Tsize t') -> Vg E i = Vg E' i. by move => i lin; apply: sd; move:(cle_ltT lin se2). have pb:forall i, i <=c nat_to_B (Tsize t3) -> Vg E i = Vg E' i. by move => i lin; apply: sd; move:(cle_ltT lin se3). move: (product_injective (He _ _ _ (Tproduct t2 t3) sa sc) (h _ sa)). by rewrite -/(Tree_value _) (Hf t' E E' pa)(Hf t3 E E' pb); case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)