CoqPiece1.v

(* plf/Equiv.v *)

Lemma aeval_weakening : forall x st a ni,
  var_not_used_in_aexp x a ->
  aeval (x !-> ni ; st) a = aeval st a.
Proof.
  intros. induction H; simpl; try congruence.
  eapply t_update_neq; eauto.
Qed.

Theorem subst_equiv_property_mk2 : forall x1 x2 a1 a2,
  var_not_used_in_aexp x1 a1 ->
  cequiv <{ x1 := a1; x2 := a2 }>
  <{ x1 := a1; x2 := subst_aexp x1 a1 a2 }>.
Proof.
  intros x1 x2 a1 a2 NOT_USED. revert x1 x2 a1 NOT_USED. induction a2; simpl; intros.
  - eapply refl_cequiv.
  - destruct (x1 =? x)%string as [ | ] eqn: H_OBS.
    + apply String.eqb_eq in H_OBS. subst x.
      assert (claim : forall st, aeval (x1 !-> aeval st a1; st) x1 = aeval (x1 !-> aeval st a1; st) a1).
      { intros st. erewrite <- aeval_weakening with (x := x1) (a := a1) (ni := aeval st x1); eauto.
        simpl. rewrite t_update_same. rewrite t_update_eq. symmetry. eapply aeval_weakening; eauto.
      }
      intros st st'. split; intros H_step.
      * inversion H_step; subst. clear H_step. rename st' into st'', st'0 into st', H1 into H_step, H4 into H_step'.
        inversion H_step; subst; clear H_step. inversion H_step'; subst; clear H_step'.
        eapply E_Seq; eapply E_Asgn; [reflexivity | eauto].
      * inversion H_step; subst. clear H_step. rename st' into st'', st'0 into st', H1 into H_step, H4 into H_step'.
        inversion H_step; subst; clear H_step. inversion H_step'; subst; clear H_step'.
        eapply E_Seq; eapply E_Asgn; [reflexivity | eauto].
    + apply String.eqb_neq in H_OBS.
      eapply CSeq_congruence; eapply refl_cequiv.
  - rename a1 into a, a2_1 into a1, a2_2 into a2, IHa2_1 into IH1, IHa2_2 into IH2.
    assert (H_a1 : cequiv <{ x1 := a; x2 := a1 }> <{ x1 := a; x2 := (subst_aexp x1 a a1) }>)
      by exact (IH1 x1 x2 a NOT_USED).
    assert (H_a2 : cequiv <{ x1 := a; x2 := a2 }> <{ x1 := a; x2 := (subst_aexp x1 a a2) }>)
      by exact (IH2 x1 x2 a NOT_USED).
    clear IH1 IH2. intros st0 st. rename x1 into x, x2 into x'. set (st1 := x !-> aeval st0 a; st0).
    specialize (H_a1 st0 (x' !-> aeval st1 a1; st1)); simpl in H_a1.
    specialize (H_a2 st0 (x' !-> aeval st1 a2; st1)); simpl in H_a2.
    split; intros H_step.
    + eapply E_Seq with (st' := st1).
      * now eapply E_Asgn.
      * inversion H_step; subst; clear H_step.
        rename H1 into H_step0, H4 into H_step1.
        inversion H_step0; subst; clear H_step0.
        inversion H_step1; subst; clear H_step1.
        destruct H_a1 as [H_a1 _], H_a2 as [H_a2 _].
        assert (claim1 : st0 =[ x := a; x' := a1 ]=> (x' !-> aeval st1 a1; st1))
          by now eapply E_Seq with (st' := st1); econstructor.
        apply H_a1 in claim1.
        inversion claim1; subst; clear claim1.
        inversion H1; subst; clear H1.
        inversion H4; subst; clear H4.
        assert (claim2 : st0 =[ x := a; x' := a2 ]=> (x' !-> aeval st1 a2; st1))
          by now eapply E_Seq with (st' := st1); econstructor.
        apply H_a2 in claim2.
        inversion claim2; subst; clear claim2.
        inversion H1; subst; clear H1.
        inversion H5; subst; clear H5.
        apply f_equal with (f := fun st : state => st x') in H3, H4; simpl in H3, H4.
        do 2 rewrite t_update_eq in H3, H4. econstructor. simpl. fold st1. now rewrite <- H3, <- H4.
    + eapply E_Seq with (st' := st1).
      * now eapply E_Asgn.
      * inversion H_step; subst; clear H_step.
        rename H1 into H_step0, H4 into H_step1.
        inversion H_step0; subst; clear H_step0.
        inversion H_step1; subst; clear H_step1.
        destruct H_a1 as [H_a1 _], H_a2 as [H_a2 _].
        assert (claim1 : st0 =[ x := a; x' := a1 ]=> (x' !-> aeval st1 a1; st1))
          by now eapply E_Seq with (st' := st1); econstructor.
        apply H_a1 in claim1.
        inversion claim1; subst; clear claim1.
        inversion H1; subst; clear H1.
        inversion H4; subst; clear H4.
        assert (claim2 : st0 =[ x := a; x' := a2 ]=> (x' !-> aeval st1 a2; st1))
          by now eapply E_Seq with (st' := st1); econstructor.
        apply H_a2 in claim2.
        inversion claim2; subst; clear claim2.
        inversion H1; subst; clear H1.
        inversion H5; subst; clear H5.
        apply f_equal with (f := fun st : state => st x') in H3, H4; simpl in H3, H4.
        do 2 rewrite t_update_eq in H3, H4. econstructor. simpl. fold st1. now rewrite <- H3, <- H4.
  - rename a1 into a, a2_1 into a1, a2_2 into a2, IHa2_1 into IH1, IHa2_2 into IH2.
    assert (H_a1 : cequiv <{ x1 := a; x2 := a1 }> <{ x1 := a; x2 := (subst_aexp x1 a a1) }>)
      by exact (IH1 x1 x2 a NOT_USED).
    assert (H_a2 : cequiv <{ x1 := a; x2 := a2 }> <{ x1 := a; x2 := (subst_aexp x1 a a2) }>)
      by exact (IH2 x1 x2 a NOT_USED).
    clear IH1 IH2. intros st0 st. rename x1 into x, x2 into x'. set (st1 := x !-> aeval st0 a; st0).
    specialize (H_a1 st0 (x' !-> aeval st1 a1; st1)); simpl in H_a1.
    specialize (H_a2 st0 (x' !-> aeval st1 a2; st1)); simpl in H_a2.
    split; intros H_step.
    + eapply E_Seq with (st' := st1).
      * now eapply E_Asgn.
      * inversion H_step; subst; clear H_step.
        rename H1 into H_step0, H4 into H_step1.
        inversion H_step0; subst; clear H_step0.
        inversion H_step1; subst; clear H_step1.
        destruct H_a1 as [H_a1 _], H_a2 as [H_a2 _].
        assert (claim1 : st0 =[ x := a; x' := a1 ]=> (x' !-> aeval st1 a1; st1))
          by now eapply E_Seq with (st' := st1); econstructor.
        apply H_a1 in claim1.
        inversion claim1; subst; clear claim1.
        inversion H1; subst; clear H1.
        inversion H4; subst; clear H4.
        assert (claim2 : st0 =[ x := a; x' := a2 ]=> (x' !-> aeval st1 a2; st1))
          by now eapply E_Seq with (st' := st1); econstructor.
        apply H_a2 in claim2.
        inversion claim2; subst; clear claim2.
        inversion H1; subst; clear H1.
        inversion H5; subst; clear H5.
        apply f_equal with (f := fun st : state => st x') in H3, H4; simpl in H3, H4.
        do 2 rewrite t_update_eq in H3, H4. econstructor. simpl. fold st1. now rewrite <- H3, <- H4.
    + eapply E_Seq with (st' := st1).
      * now eapply E_Asgn.
      * inversion H_step; subst; clear H_step.
        rename H1 into H_step0, H4 into H_step1.
        inversion H_step0; subst; clear H_step0.
        inversion H_step1; subst; clear H_step1.
        destruct H_a1 as [H_a1 _], H_a2 as [H_a2 _].
        assert (claim1 : st0 =[ x := a; x' := a1 ]=> (x' !-> aeval st1 a1; st1))
          by now eapply E_Seq with (st' := st1); econstructor.
        apply H_a1 in claim1.
        inversion claim1; subst; clear claim1.
        inversion H1; subst; clear H1.
        inversion H4; subst; clear H4.
        assert (claim2 : st0 =[ x := a; x' := a2 ]=> (x' !-> aeval st1 a2; st1))
          by now eapply E_Seq with (st' := st1); econstructor.
        apply H_a2 in claim2.
        inversion claim2; subst; clear claim2.
        inversion H1; subst; clear H1.
        inversion H5; subst; clear H5.
        apply f_equal with (f := fun st : state => st x') in H3, H4; simpl in H3, H4.
        do 2 rewrite t_update_eq in H3, H4. econstructor. simpl. fold st1. now rewrite <- H3, <- H4.
  - rename a1 into a, a2_1 into a1, a2_2 into a2, IHa2_1 into IH1, IHa2_2 into IH2.
    assert (H_a1 : cequiv <{ x1 := a; x2 := a1 }> <{ x1 := a; x2 := (subst_aexp x1 a a1) }>)
      by exact (IH1 x1 x2 a NOT_USED).
    assert (H_a2 : cequiv <{ x1 := a; x2 := a2 }> <{ x1 := a; x2 := (subst_aexp x1 a a2) }>)
      by exact (IH2 x1 x2 a NOT_USED).
    clear IH1 IH2. intros st0 st. rename x1 into x, x2 into x'. set (st1 := x !-> aeval st0 a; st0).
    specialize (H_a1 st0 (x' !-> aeval st1 a1; st1)); simpl in H_a1.
    specialize (H_a2 st0 (x' !-> aeval st1 a2; st1)); simpl in H_a2.
    split; intros H_step.
    + eapply E_Seq with (st' := st1).
      * now eapply E_Asgn.
      * inversion H_step; subst; clear H_step.
        rename H1 into H_step0, H4 into H_step1.
        inversion H_step0; subst; clear H_step0.
        inversion H_step1; subst; clear H_step1.
        destruct H_a1 as [H_a1 _], H_a2 as [H_a2 _].
        assert (claim1 : st0 =[ x := a; x' := a1 ]=> (x' !-> aeval st1 a1; st1))
          by now eapply E_Seq with (st' := st1); econstructor.
        apply H_a1 in claim1.
        inversion claim1; subst; clear claim1.
        inversion H1; subst; clear H1.
        inversion H4; subst; clear H4.
        assert (claim2 : st0 =[ x := a; x' := a2 ]=> (x' !-> aeval st1 a2; st1))
          by now eapply E_Seq with (st' := st1); econstructor.
        apply H_a2 in claim2.
        inversion claim2; subst; clear claim2.
        inversion H1; subst; clear H1.
        inversion H5; subst; clear H5.
        apply f_equal with (f := fun st : state => st x') in H3, H4; simpl in H3, H4.
        do 2 rewrite t_update_eq in H3, H4. econstructor. simpl. fold st1. now rewrite <- H3, <- H4.
    + eapply E_Seq with (st' := st1).
      * now eapply E_Asgn.
      * inversion H_step; subst; clear H_step.
        rename H1 into H_step0, H4 into H_step1.
        inversion H_step0; subst; clear H_step0.
        inversion H_step1; subst; clear H_step1.
        destruct H_a1 as [H_a1 _], H_a2 as [H_a2 _].
        assert (claim1 : st0 =[ x := a; x' := a1 ]=> (x' !-> aeval st1 a1; st1))
          by now eapply E_Seq with (st' := st1); econstructor.
        apply H_a1 in claim1.
        inversion claim1; subst; clear claim1.
        inversion H1; subst; clear H1.
        inversion H4; subst; clear H4.
        assert (claim2 : st0 =[ x := a; x' := a2 ]=> (x' !-> aeval st1 a2; st1))
          by now eapply E_Seq with (st' := st1); econstructor.
        apply H_a2 in claim2.
        inversion claim2; subst; clear claim2.
        inversion H1; subst; clear H1.
        inversion H5; subst; clear H5.
        apply f_equal with (f := fun st : state => st x') in H3, H4; simpl in H3, H4.
        do 2 rewrite t_update_eq in H3, H4. econstructor. simpl. fold st1. now rewrite <- H3, <- H4.
Qed.

Lang.v

Require Import Coq.Strings.BinaryString.
Require Import Coq.Strings.Byte.
Require Import Coq.Strings.String.
Require Import Coq.ZArith.BinInt.
Require Import DschingisKhan.Prelude.Prelude.

Lemma string_length_wf_ind {A : Type} (phi : list A -> Prop)
  (IND : forall s : list A, (forall s' : list A, length s' < length s -> phi s') -> phi s)
  : forall s, phi s.
Proof.
  pose proof (@preimage_preserves_wf) as REC.
  specialize REC with (A := list A) (B := nat) (R := Nat.lt) (f := @length A).
  exact (transfinite_induction (REC lt_wf) IND).
Qed.

Module LANG1.

Import MyNotations.

Variant alphabet : Set := L | R.

#[local] Notation string := (list alphabet).
#[local] Notation lang := (ensemble string).
#[local] Infix " \in " := E.In : type_scope.

#[local]
Instance alphabet_hasEqDec
  : hasEqDec alphabet.
Proof.
  change (forall lhs : alphabet, forall rhs : alphabet, {lhs = rhs} + {lhs <> rhs}).
  decide equality.
Defined.

Inductive L_cfg1 : lang :=
| cfg1_rule1
  : [] \in L_cfg1
| cfg1_rule2 (str : string)
  (H_str : str \in L_cfg1)
  : [L] ++ str ++ [R] \in L_cfg1
| cfg1_rule3 (str : string)
  (H_str : str \in L_cfg1)
  : [R] ++ str ++ [L] \in L_cfg1
| cfg1_rule4 (str1 : string) (str2 : string)
  (H_str1 : str1 \in L_cfg1)
  (H_str2 : str2 \in L_cfg1)
  : str1 ++ str2 \in L_cfg1.

#[local] Hint Constructors L_cfg1 : core.

#[local] Notation count a s := (count_occ eq_dec s a).

Variant cfg1_spec (LANG : lang) : Prop :=
  cfg1_lang_spec
  (nL_eq_nR : forall str, str \in LANG <-> count L str = count R str)
  : cfg1_spec LANG.

Section THEORY.

Lemma count_app (a : alphabet) (s : string) (s' : string)
  : count a (s ++ s') = count a s + count a s'.
Proof. revert a s'; induction s as [ | [ | ] s IH]; intros [ | ] s'; simpl; eauto. Qed.

Lemma count_app_cancel_l (a : alphabet) (s : string) (s' : string) (n : nat) (n' : nat)
  (H_s_app_s' : count a (s ++ s') = n + n')
  (H_s : count a s = n)
  : count a s' = n'.
Proof. revert a s' n n' H_s_app_s' H_s; induction s as [ | [ | ] s IH]; intros [ | ]; simpl; i; subst n; eauto. Qed.

Lemma count_app_cancel_r (a : alphabet) (s : string) (s' : string) (n : nat) (n' : nat)
  (H_s_app_s' : count a (s ++ s') = n + n')
  (H_s' : count a s' = n')
  : count a s = n.
Proof.
  subst n'. revert a s' n H_s_app_s'. induction s' as [ | [ | ] s' IH] using List.rev_ind; simpl; i.
  all: try rewrite Nat.add_0_r in *; try rewrite app_nil_r in *; eauto.
  all: erewrite count_occ_app with (l1 := s) (l2 := s' ++ [_]) in H_s_app_s'; lia.
Qed.

Inductive isLast (a : alphabet) : string -> Prop :=
| isLast_1
  : isLast a [a]
| isLast_S (a' : alphabet) (s : string)
  (H_isLast : isLast a s)
  : isLast a (a' :: s).

#[local] Hint Constructors isLast : core.

Lemma isLast_thm (a : alphabet) (s : string)
  (H_isLast : isLast a s)
  : exists s', s = s' ++ [a].
Proof.
  induction H_isLast as [ | a' s H_isLast [s' IH]].
  - exists []; eauto.
  - rewrite IH. exists (a' :: s'). reflexivity. 
Qed.

Variant string_cut (s : string) : Prop :=
  string_cut_intro (s_prefix : string) (s' : string)
  (H_app : s = s_prefix ++ s')
  (H_len : length s' > 0)
  (H_cut : count L s' = count R s')
  : string_cut s.

Lemma if_count_L_s_lt_count_R_s (s : string)
  (count_L_s_lt_count_R_s : count L s < count R s)
  : string_cut s \/ isLast R s.
Proof with eauto.
  revert count_L_s_lt_count_R_s; induction s as [ | [ | ] s IH]; simpl; try lia; i.
  - assert (IH_supply : count L s < count R s) by lia. apply IH in IH_supply.
    clear IH. destruct IH_supply as [IH | IH]...
    inversion IH; subst. left. eapply string_cut_intro with (s' := s') (s_prefix := L :: s_prefix)...
  - assert (count L s = count R s \/ count L s < count R s) as [IH_supply | IH_supply] by lia.
    + destruct s as [ | a' s']...
      left. eapply string_cut_intro with (s' := a' :: s') (s_prefix := [R])... simpl; lia.
    + apply IH in IH_supply. clear IH; destruct IH_supply as [IH | IH]...
      left. inversion IH; subst. eapply string_cut_intro with (s' := s') (s_prefix := R :: s_prefix)...
Qed.

Lemma if_count_L_s_gt_count_R_s (s : string)
  (count_L_s_gt_count_R_s : count L s > count R s)
  : string_cut s \/ isLast L s.
Proof with eauto.
  revert count_L_s_gt_count_R_s; induction s as [ | [ | ] s IH]; simpl; try lia; i.
  - assert (count L s = count R s \/ count L s > count R s) as [IH_supply | IH_supply] by lia.
    + destruct s as [ | a' s']...
      left. eapply string_cut_intro with (s' := a' :: s') (s_prefix := [L])... simpl; lia.
    + apply IH in IH_supply. clear IH; destruct IH_supply as [IH | IH]...
      left. inversion IH; subst. eapply string_cut_intro with (s' := s') (s_prefix := L :: s_prefix)...
  - assert (IH_supply : count L s > count R s) by lia. apply IH in IH_supply.
    clear IH. destruct IH_supply as [IH | IH]...
    inversion IH; subst. left. eapply string_cut_intro with (s' := s') (s_prefix := R :: s_prefix)...
Qed.

Theorem cfg1_completeness (s : string)
  (count_L_eq_count_R : count L s = count R s)
  : s \in L_cfg1.
Proof with eauto.
  revert count_L_eq_count_R. induction s as [[ | [ | ] s] IH] using string_length_wf_ind; simpl in *...
  - i. assert (count_L_s_lt_count_R_s : count L s < count R s) by lia.
    apply if_count_L_s_lt_count_R_s in count_L_s_lt_count_R_s.
    destruct count_L_s_lt_count_R_s as [[? ? ? ? ?] | H_last_R].
    + assert (IH_supply1 : length s' < S (length s)) by now pose proof (@app_length _ s_prefix s'); subst s; lia.
      pose proof (IH s' IH_supply1 H_cut) as H_s'.
      assert (IH_supply2 : length (L :: s_prefix) < S (length s)) by now simpl; pose proof (@app_length _ s_prefix s'); subst s; lia.
      assert (CLAIM : count L (L :: s_prefix) = count R (L :: s_prefix)).
      { eapply count_app_cancel_r with (s := L :: s_prefix) (s' := s') (n' := count R s')...
        simpl. rewrite <- H_app. rewrite <- count_app. rewrite <- H_app...
      }
      assert (H_prefix : L :: s_prefix \in L_cfg1).
      { eapply IH... }
      rewrite H_app. eapply cfg1_rule4 with (str1 := L :: s_prefix) (str2 := s')...
    + apply isLast_thm in H_last_R. destruct H_last_R as [s' ->]; simpl in *.
      eapply cfg1_rule2. eapply IH.
      { replace (length (s' ++ [R])) with (length (rev (R :: rev s'))) by now simpl; f_equal; rewrite rev_involutive.
        rewrite rev_length. simpl. rewrite rev_length. lia.
      }
      { rewrite <- rev_involutive with (l := s' ++ [R]) in count_L_eq_count_R.
        rewrite -> rev_unit in count_L_eq_count_R. do 2 rewrite count_occ_rev in count_L_eq_count_R.
        simpl in count_L_eq_count_R. apply f_equal with (f := Nat.pred) in count_L_eq_count_R.
        simpl in count_L_eq_count_R. do 2 rewrite count_occ_rev in count_L_eq_count_R...
      }
  - i. assert (count_L_s_gt_count_R_s : count L s > count R s) by lia.
    apply if_count_L_s_gt_count_R_s in count_L_s_gt_count_R_s.
    destruct count_L_s_gt_count_R_s as [[? ? ? ? ?] | H_last_L].
    + assert (IH_supply1 : length s' < S (length s)) by now pose proof (@app_length _ s_prefix s'); subst s; lia.
      pose proof (IH s' IH_supply1 H_cut) as H_s'.
      assert (IH_supply2 : length (R :: s_prefix) < S (length s)) by now simpl; pose proof (@app_length _ s_prefix s'); subst s; lia.
      assert (CLAIM : count L (R :: s_prefix) = count R (R :: s_prefix)).
      { eapply count_app_cancel_r with (s := R :: s_prefix) (s' := s') (n' := count R s')...
        simpl. rewrite <- H_app. rewrite <- count_app. rewrite <- H_app...
      }
      assert (H_prefix : R :: s_prefix \in L_cfg1).
      { eapply IH... }
      rewrite H_app. eapply cfg1_rule4 with (str1 := R :: s_prefix) (str2 := s')...
    + apply isLast_thm in H_last_L. destruct H_last_L as [s' ->]; simpl in *.
      eapply cfg1_rule3. eapply IH.
      { replace (length (s' ++ [L])) with (length (rev (L :: rev s'))) by now simpl; f_equal; rewrite rev_involutive.
        rewrite rev_length. simpl. rewrite rev_length. lia.
      }
      { rewrite <- rev_involutive with (l := s' ++ [L]) in count_L_eq_count_R.
        rewrite -> rev_unit in count_L_eq_count_R. do 2 rewrite count_occ_rev in count_L_eq_count_R.
        simpl in count_L_eq_count_R. apply f_equal with (f := Nat.pred) in count_L_eq_count_R.
        simpl in count_L_eq_count_R. do 2 rewrite count_occ_rev in count_L_eq_count_R...
      }
Qed.

Theorem cfg1_generates_L_cfg1_as_wanted
  : cfg1_spec L_cfg1.
Proof with eauto.
  split. intros s. split.
  - intros H_in; induction H_in as [ | s1 H_in1 IH1 | s2 H_in2 IH2 | s1 s2 H_in1 IH1 H_in2 IH2 ]; simpl; eauto.
    + rewrite <- rev_involutive with (l := s1 ++ [R]). rewrite rev_unit.
      do 2 rewrite count_occ_rev. simpl. do 2 rewrite count_occ_rev...
    + rewrite <- rev_involutive with (l := s2 ++ [L]). rewrite rev_unit.
      do 2 rewrite count_occ_rev. simpl. do 2 rewrite count_occ_rev...
    + do 2 rewrite count_occ_app...
  - exact (cfg1_completeness s). 
Qed.

End THEORY.

End LANG1.

Module LANG2.

Inductive strSQLElem : Set :=
| Text : string -> strSQLElem
| Hole : string -> strSQLElem.

Inductive value : Set :=
| ColName : string -> value
| StrVal  : string -> value
| IntVal  : Z      -> value
| Var     : string -> value.

Inductive term : Set := 
| equalTerm : value -> value -> term.

Inductive pred : Set := 
| orPred : pred -> pred -> pred
| termPred : term -> pred.

Inductive cols : Set :=
| star : cols
| colNames : list string -> cols.

Inductive sql : Set :=
| sqlSFW : cols -> string -> option pred -> sql.

End LANG2.
  

Stream1.v

Require Import Coq.Lists.Streams.

CoFixpoint xs (n: nat) : Stream nat :=
  Cons n (xs (2 + n)).

Inductive even : nat -> Prop :=
| even_0
  : even 0
| even_2_plus_n (n: nat)
  (EVEN: even n)
  : even (2 + n).

CoInductive all_even (ns: Stream nat) : Prop :=
  { all_even_hd: even (hd ns); all_even_tl: all_even (tl ns) }.

Lemma xs_all_even (n: nat)
  (EVEN: even n)
  : all_even (xs n).
Proof.
  revert n EVEN. cofix CIH; intros.
  econstructor; simpl.
  - exact EVEN.
  - eapply CIH. econstructor 2. exact EVEN.
Qed.

Lemma Forall_xs_xs_even (n: nat)
  (EVEN: even n)
  : ForAll all_even (xs n).
Proof.
  revert n EVEN. cofix CIH; intros.
  econstructor.
  - eapply xs_all_even. exact EVEN.
  - simpl. eapply CIH. econstructor 2. exact EVEN.
Qed.