proposition: Lemma equiv_bool_ok : forall t1 t2, match equiv_bool t1 t2 with true => equiv t1 t2 | false => ~equiv t1 t2 end.
proof: Proof. intros t1; pattern t1; apply term_rec3; clear t1. intros v1 t2; case t2; clear t2. intro v2; rewrite equiv_bool_equation; generalize (X.eq_bool_ok v1 v2); case (X.eq_bool v1 v2). intro v1_eq_v2; rewrite v1_eq_v2; apply Eq. intros v1_diff_v2 v1_eq_v2; apply v1_diff_v2; inversion v1_eq_v2; reflexivity. intros f2 l2; rewrite equiv_bool_equation; intro t1_eq_t2; inversion t1_eq_t2. intros f1 l1 IH t2; case t2; clear t2. intros v2; rewrite equiv_bool_equation; intro t1_eq_t2; inversion t1_eq_t2. intros f2 l2; rewrite equiv_bool_equation. case_eq (prec_eq_bool Prec f1 f2). intro f1_eq_f2; case_eq (status Prec f1). intro Lex_f1; simpl. assert (H : if (fix equiv_lex_bool (kk1 kk2 : list term) : bool := match kk1 with | [] => match kk2 with | [] => true | _ :: _ => false end | t1 :: k1 => match kk2 with | [] => false | t2 :: k2 => equiv_bool t1 t2 && equiv_lex_bool k1 k2 end end) l1 l2 then equiv_list_lex l1 l2 else ~equiv_list_lex l1 l2). revert l2; induction l1 as [ | a1 l1]; intro l2; case l2; clear l2. apply Eq_list_nil. intros a2 l2; simpl; intro l1_eq_l2; inversion l1_eq_l2. simpl; intro l1_eq_l2; inversion l1_eq_l2. intros a2 l2; simpl; generalize (IH a1 (or_introl _ (eq_refl _)) a2). case (equiv_bool a1 a2). intro a1_eq_a2; generalize (IHl1 (tail_prop _ IH) l2). simpl. case ((fix equiv_lex_bool (kk1 kk2 : list term) : bool := match kk1 with | [] => match kk2 with | [] => true | _ :: _ => false end | t1 :: k1 => match kk2 with | [] => false | t3 :: k2 => equiv_bool t1 t3 && equiv_lex_bool k1 k2 end end) l1 l2). intro l1_eq_l2; apply Eq_list_cons; assumption. intros l1_diff_l2 l1_eq_l2; apply l1_diff_l2; inversion l1_eq_l2; assumption. intros a1_diff_a2 l1_eq_l2; apply a1_diff_a2; inversion l1_eq_l2; assumption. revert H; simpl. case ((fix equiv_lex_bool (kk1 kk2 : list term) : bool := match kk1 with | [] => match kk2 with | [] => true | _ :: _ => false end | t1 :: k1 => match kk2 with | [] => false | t3 :: k2 => equiv_bool t1 t3 && equiv_lex_bool k1 k2 end end) l1 l2). intro l1_eq_l2. apply Eq_lex; trivial. assert (H2:= prec_eq_bool_ok). assert (H2':= H2 symbol Prec f1 f2). rewrite f1_eq_f2 in H2'. assert (H5:= prec_eq_status Prec f1 f2). assert (H6: status Prec f1 = status Prec f2). apply H5; trivial. rewrite <- H6. trivial. assert (H2:= prec_eq_bool_ok). assert (H2':= (H2 symbol Prec f1 f2)). rewrite f1_eq_f2 in H2'. trivial. intros l1_diff_l2 t1_eq_t2; inversion t1_eq_t2; subst l2. apply l1_diff_l2; generalize l1; intro l; induction l as [ | a l]. apply Eq_list_nil. apply Eq_list_cons; [apply Eq | assumption]. apply l1_diff_l2; assumption. subst f2; rewrite Lex_f1 in H3. discriminate. intro Mul_f1; simpl. assert (H : if (fix equiv_mult_bool (kk1 kk2 : list term) : bool := match kk1 with | [] => match kk2 with | [] => true | _ :: _ => false end | t1 :: k1 => match remove equiv_bool t1 kk2 with | Some k2 => equiv_mult_bool k1 k2 | None => false end end) l1 l2 then permut0 equiv l1 l2 else ~permut0 equiv l1 l2). revert l2; induction l1 as [ | a1 l1]. intro l2; case l2; clear l2. simpl; apply Pnil. intros a2 l2; simpl; intro t1_eq_t2; inversion t1_eq_t2. assert (R : forall l2, match remove equiv_bool a1 l2 with | Some _ => {a2 : term & {l2' : list term & {l2'' : list term | equiv a1 a2 /\ l2 = l2' ++ a2 :: l2'' /\ remove equiv_bool a1 l2 = Some (l2' ++ l2'')}}} | None => forall a2, equiv a1 a2 -> ~ In a2 l2 end). intro l2; induction l2 as [ | a2 l2]. intros a2 a1_eq_a2 F; assumption. rewrite remove_equation. generalize (IH a1 (or_introl _ (eq_refl _)) a2); case (equiv_bool a1 a2). intro a1_eq_a2; exists a2; exists (@nil term); exists l2; repeat split; assumption. intro a1_diff_a2; revert IHl2; case (remove equiv_bool a1 l2). intros k2 [a1' [l2' [l2'' [H1 [H2 H3]]]]]; exists a1'; exists (a2 :: l2'); exists l2''; repeat split. assumption. simpl; apply f_equal; assumption. simpl; do 2 apply f_equal; injection H3; intros; assumption. simpl; intros a1_not_in_l2; intros a a_eq_a1 [a_eq_a2 | a_in_l2]. subst a; apply a1_diff_a2; assumption. apply (a1_not_in_l2 a a_eq_a1 a_in_l2). intro l2; generalize (R l2); case (remove equiv_bool a1 l2). intros k2 [a2 [k2' [k2'' [H1 [H2 H3]]]]]. generalize (IHl1 (tail_prop _ IH) k2); simpl. injection H3; clear H3; intro H3; case ((fix equiv_mult_bool (kk1 kk2 : list term) : bool := match kk1 with | [] => match kk2 with | [] => true | _ :: _ => false end | t1 :: k1 => match remove equiv_bool t1 kk2 with | Some k3 => equiv_mult_bool k1 k3 | None => false end end) l1 k2). intro P; subst l2 k2; apply Pcons; assumption. intros not_P P; subst l2 k2; apply not_P. apply (@permut_cons_inside term term equiv) with a1 a2. intros u3 u1 u4 u2 _ _ _ _ H31 H41 H42; transitivity u1. assumption. transitivity u4. symmetry; assumption. assumption. assumption. assumption. intros H P; inversion P as [ | a1' a2 l1' l2' l2'' a1_eq_a2 P']. apply (H a2 a1_eq_a2); subst l2; apply in_or_app; right; left; reflexivity. revert H; case ((fix equiv_mult_bool (kk1 kk2 : list term) : bool := match kk1 with | [] => match kk2 with | [] => true | _ :: _ => false end | t1 :: k1 => match remove equiv_bool t1 kk2 with | Some k2 => equiv_mult_bool k1 k2 | None => false end end) l1 l2). intro P. apply Eq_mul. assumption. assert (H2:= prec_eq_bool_ok). assert (H2':= H2 symbol Prec f1 f2). rewrite f1_eq_f2 in H2'. assert (H6:= prec_eq_status Prec f1 f2); trivial. assert (H7: status Prec f1 = status Prec f2). apply H6. trivial. rewrite <- H7. trivial. assert (H2:= prec_eq_bool_ok). assert (H2':= H2 symbol Prec f1 f2). rewrite f1_eq_f2 in H2'. trivial. trivial. intros not_P t1_eq_t2. inversion t1_eq_t2. subst l2. apply not_P; apply permut_refl; intros; reflexivity. rewrite Mul_f1 in H3; discriminate. apply not_P; assumption. intros f1_diff_f2 t1_eq_t2. inversion t1_eq_t2. rewrite H1 in f1_diff_f2. assert (H3:= prec_eq_bool_ok). assert (H3':= H3 symbol Prec f2 f2). rewrite f1_diff_f2 in H3'. contradict H3'. apply prec_eq_refl. trivial. assert (H8:= prec_eq_bool_ok). assert (H8':= H8 symbol Prec f1 f2). rewrite f1_diff_f2 in H8'. contradict H8'. trivial. assert (H8:= prec_eq_bool_ok). assert (H8':= H8 symbol Prec f1 f2). rewrite f1_diff_f2 in H8'. contradict H8'. trivial. Defined.
imports: Coq(Bool Peano List PeanoNat) CoLoR(closure more_list equiv_list list_permut dickson) Coq(Relations Wellfounded Arith Wf_nat Recdef Program Morphisms Lia) CoLoR(term_spec term decidable_set ordered_set NatCompat)