Stream: Coq users

Topic: ✔ Split list into 3 parts in proof

Julin Shaji (Mar 13 2024 at 14:37):

Given a list, while doing case analysis in proof mode, is there a way
to split like [], [a], a::l' instead of the usual [], a::l'?

For a scenario like this:

Require Import List ssreflect.
Import ListNotations.

Goal forall (A:Type) (l : list A),
  match l with
  | [] => 0
  | [a] => 1
  | _ => 2
  end = length l.
Proof.
  move => A l.
  case l.
  - by [].
  - move => a2 w2.
    case w2.
    + by [].
    + move => a3 w3.
      by [].

Pierre Roux (Mar 13 2024 at 14:40):

move=> A [| a [| l']]

Julin Shaji (Mar 13 2024 at 14:50):

Thanks!

Notification Bot (Mar 13 2024 at 14:50):

Julin Shaji has marked this topic as resolved.

Meven Lennon-Bertrand (Mar 13 2024 at 15:35):

In vanilla Coq, intros A [|a [|l']]. does the same

Last updated: Oct 13 2024 at 01:02 UTC