proposition: Lemma remove_equiv_list_is_sound : forall l1 l2, match remove_equiv_list l1 l2 with | (l1',l2') => {lc | permut0 equiv l1 (l1' ++ lc) /\ permut0 equiv l2 (l2' ++ lc) /\ (forall t1 t2, mem equiv t1 l1' -> mem equiv t2 l2' -> ~ equiv t1 t2)} end.
proof: Proof. intros l1 l2; functional induction (remove_equiv_list l1 l2) as [ l1 | H1 l2 H2 H3 H4 H' | H1 l2 t1 l1 H2 H3 H4 _ l2' H IH | H1 l2 t1 l1 H2 H3 H4 H' H IH l1' l2' R]. exists (@nil term); simpl; repeat split; reflexivity || auto. rewrite <- app_nil_end; reflexivity || auto. destruct l2 as [ | t2 l2]. contradiction. exists (@nil term); simpl; repeat split; reflexivity || auto. rewrite <- app_nil_end; reflexivity || auto. destruct (@remove_equiv_is_sound_some t1 l2 l2' H) as [t2 [t1_eq_t2 P2]]. destruct (remove_equiv_list l1 l2') as [l1'' l2'']. destruct IH as [lc [P1 [P2' D]]]. exists (t1 :: lc); repeat split; reflexivity || auto. rewrite <- permut0_cons_inside; trivial. apply equiv_equiv. reflexivity. rewrite P2; rewrite <- permut0_cons_inside; trivial. apply equiv_equiv. symmetry; trivial. rewrite R in IH. destruct IH as [lc [P1 [P2 D]]]. exists lc; repeat split; auto. simpl; rewrite <- permut0_cons; trivial. apply equiv_equiv. reflexivity. intros u1 u2 [t1_eq_u1 | u1_mem_l1'] u2_mem_u2'. assert (H'' := @remove_equiv_is_sound_none t1 l2 H). intro u1_eq_u2; apply (H'' u2). rewrite P2; rewrite <- mem_or_app; left; trivial. transitivity u1; trivial. symmetry; trivial. apply D; trivial. Qed.
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)