Can someone help with the proof?

Using Coq
1

So I have this proof which I have no idea how to prove. I believe that solution should be instructive.

Set Implicit Arguments.
Require Import Arith Omega List Bool.

Fixpoint nat_eqb (n m: nat): bool :=
  match n, m with
  | O, O => true
  | S n', S m' => nat_eqb n' m'
  | _, _ => false
  end.

Theorem nat_eq_reflect: forall n m, reflect (n = m) (nat_eqb n m).
Proof.
  refine (fix aux n m :=
    match n, m with
    | O, O => _
    | S n', S m' => _
    | _, _ => _
    end).
  + apply ReflectT. auto.
  + apply ReflectF. intuition.
  + apply ReflectF. intuition.
  + simpl. destruct (aux n' m').
    - apply ReflectT. subst. auto.
    - apply ReflectF. congruence.
Qed.

Definition In_bool A (x: A) (L: list A) (beq: A -> A -> bool): bool.
Proof.
  induction L.
  + exact false.
  + exact (orb (beq x a) IHL).
Defined.

Theorem In_reflect A (x: A) (L: list A) (beq: A -> A -> bool) (H: forall x y, reflect (x = y) (beq x y)):
    reflect (In x L) (In_bool x L beq).
Proof.
  induction L.
  + simpl. apply ReflectF. auto.
  + simpl. destruct (H a x).
    - subst. assert (beq x x = true). destruct (H x x); auto.
      rewrite H0. simpl. apply ReflectT. left. auto.
    - destruct IHL.
      * replace (beq x a || true) with true by intuition. apply ReflectT. auto.
      * assert (beq x a = false). destruct (H x a); congruence.
        rewrite H0. simpl. apply ReflectF. tauto.
Qed.

Definition aux2_bool (n: nat) (L: list nat): bool.
Proof.
  pose (seq 0 n) as l. induction l.
  + exact true.
  + exact (if (In_bool a L nat_eqb) then IHl else false).
Defined.

Theorem aux2_reflect (n: nat) (L: list nat): reflect (forall x, x < n -> In x L) (aux2_bool n L).
Proof.
  unfold aux2_bool.
Admitted.
2

There is no need to use induction in the definition of aux2_bool. You can use the predefined function forallb:

Definition aux2_bool' (n : nat) (L: list nat) :=
  forallb (fun x => In_bool x L nat_eqb) (seq 0 n).

Lemma forallb_reflect (X : Type) (f : X -> bool) (xs : list X) :
  reflect (forall x, In x xs -> f x = true) (forallb f xs).
Proof.
  induction xs.
  - cbn. left. tauto.
  - cbn. destruct (f a) eqn:E; cbn.
    + destruct IHxs.
      * left. intros x [-> | H]; auto.
      * right. intuition.
    + right. intros H. specialize (H a (or_introl eq_refl)). congruence.
Qed.

Theorem aux2'_reflect (n: nat) (L: list nat): reflect (forall x, x < n -> In x L) (aux2_bool' n L).
Proof.
  unfold aux2_bool'.
  pose proof forallb_reflect (fun x => In_bool x L nat_eqb) (seq 0 n) as [H|H].
  - left. intros x Hx.
    assert (In x (seq 0 n)) as Haux.
    { replace x with (x + 0) by omega. apply in_seq. omega. }
    specialize H with (1 := Haux).
    rewrite reflect_iff; eauto.
    apply In_reflect. intros. apply nat_eq_reflect.
  - right. intros H'. contradict H.
    intros x Hx.
    assert (x < n) as Haux.
    { apply in_seq in Hx. omega. }
    specialize H' with (1 := Haux).
    rewrite reflect_iff in H'; eauto.
    apply In_reflect. intros. apply nat_eq_reflect.
Qed.

EDIT/PS:

Lemma nat_eq_reflect can be simplified using induction instead of fix. I usually try to avoid doing induction using fixpoints. Also, note that I used the tactics left and right instead of apply ReflectT and apply ReflectF. (But that’s probably a matter of taste; I often have the problem to confuse left and right, so apply is also good).

Theorem nat_eq_reflect: forall n m, reflect (n = m) (nat_eqb n m).
Proof.
  intros n. induction n as [ | n' IH]; intros [ | m']; cbn in *.
  - left. reflexivity.
  - right. omega.
  - right. omega.
  - specialize (IH m') as [IH|IH].
    + left. omega.
    + right. omega.
Qed.
1 Like