未解決問題_range_Forall.v

Require Import Arith List.
Import ListNotations.

Fixpoint range_aux (a len: nat) : list nat :=
  match len with
  | O => []
  | S len' => a :: range_aux (S a) len'
  end.
Definition range (a b: nat) : list nat := range_aux a (b - a + 1).

Lemma range_Forall : forall a b,
    Forall (fun x => a <= x <= b) (range a b).
Proof.
  (* 未解決 *)
Admitted.

Definition range (a b: nat) : list nat := range_aux a (b + 1 - a). (* -aの位置を後ろにずらした *)
にしないと b < a のときにrange_auxがaのリストを作るのでrange_Forallが成り立ちません。
（Eval compute in (range 4 3). では[4]が出ます）
rangeの定義を上のものに変更するか、range_Forallの前提にa <= bを入れる必要があります。

おお！ありがとうございます！
(b + 1 - a) の方針に修正します！