Require Import List Undecidability.Shared.ListAutomation Lia.
Import ListNotations ListAutomationNotations.
Fixpoint count (l : list nat) (n : nat) :=
match l with
| [] => 0
| m :: l => if Nat.eqb n m then S (count l n) else count l n
end.
Lemma countSplit (A B: list nat) (x: nat) : count A x + count B x = count (A ++ B) x.
Proof.
induction A.
- reflexivity.
- cbn. destruct (Nat.eqb x a).
+ cbn. f_equal; exact IHA.
+ exact IHA.
Qed.
Lemma notInZero (x: nat) A :
not (x el A) <-> count A x = 0.
Proof.
split; induction A.
- reflexivity.
- intros H. cbn in *. destruct (PeanoNat.Nat.eqb_spec x a).
+ exfalso. apply H. left. congruence.
+ apply IHA. intros F. apply H. now right.
- tauto.
- cbn. destruct (PeanoNat.Nat.eqb_spec x a).
+ subst a. lia.
+ intros H [E | E].
* now symmetry in E.
* tauto.
Qed.
Section fix_X.
Variable X:Type.
Implicit Types (A B: list X) (a b c: X).
Lemma last_app_eq A B a b :
A++[a] = B++[b] -> A = B /\ a = b.
Proof.
intros H%(f_equal (@rev X)). rewrite !rev_app_distr in H. split.
- inv H. apply (f_equal (@rev X)) in H2. now rewrite !rev_involutive in H2.
- now inv H.
Qed.
Lemma rev_eq A B:
List.rev A = List.rev B <-> A = B.
Proof.
split.
- intros H%(f_equal (@rev X)). now rewrite !rev_involutive in H.
- now intros <-.
Qed.
Lemma rev_nil A:
rev A = [] -> A = [].
Proof.
destruct A. auto. now intros H%eq_sym%app_cons_not_nil.
Qed.
End fix_X.
Import ListNotations ListAutomationNotations.
Fixpoint count (l : list nat) (n : nat) :=
match l with
| [] => 0
| m :: l => if Nat.eqb n m then S (count l n) else count l n
end.
Lemma countSplit (A B: list nat) (x: nat) : count A x + count B x = count (A ++ B) x.
Proof.
induction A.
- reflexivity.
- cbn. destruct (Nat.eqb x a).
+ cbn. f_equal; exact IHA.
+ exact IHA.
Qed.
Lemma notInZero (x: nat) A :
not (x el A) <-> count A x = 0.
Proof.
split; induction A.
- reflexivity.
- intros H. cbn in *. destruct (PeanoNat.Nat.eqb_spec x a).
+ exfalso. apply H. left. congruence.
+ apply IHA. intros F. apply H. now right.
- tauto.
- cbn. destruct (PeanoNat.Nat.eqb_spec x a).
+ subst a. lia.
+ intros H [E | E].
* now symmetry in E.
* tauto.
Qed.
Section fix_X.
Variable X:Type.
Implicit Types (A B: list X) (a b c: X).
Lemma last_app_eq A B a b :
A++[a] = B++[b] -> A = B /\ a = b.
Proof.
intros H%(f_equal (@rev X)). rewrite !rev_app_distr in H. split.
- inv H. apply (f_equal (@rev X)) in H2. now rewrite !rev_involutive in H2.
- now inv H.
Qed.
Lemma rev_eq A B:
List.rev A = List.rev B <-> A = B.
Proof.
split.
- intros H%(f_equal (@rev X)). now rewrite !rev_involutive in H.
- now intros <-.
Qed.
Lemma rev_nil A:
rev A = [] -> A = [].
Proof.
destruct A. auto. now intros H%eq_sym%app_cons_not_nil.
Qed.
End fix_X.