The Coq mailing list

[Maximilian Wuttke <mwuttke97 AT posteo.de>]

On 30/09/2020 21:38, Agnishom Chattopadhyay wrote:
> Fixpoint fromList (l : list A) (lgt0 : length l > 0) : nonEmpty A.
>     refine (match l with
>             | nil => _
>             | (cons x nil) => singleton x
>             | (cons x xs) => consNE x (fromList xs _ )
>             end).
> 
> I am not sure how to prove these goals because of the same reasons.

First of all, you have to use the convoy pattern, that means that you
introduce the proof of 'length l > 0' *after* you make the case
distinction on l. Let me do this for you, and then we can even prove the
goals:

```
Fixpoint fromList (l : list A) : length l > 0 -> nonEmpty A.
  refine (match l with
          | nil => fun (H : length nil > 0) => _
          | (cons x nil) => fun (_ : length (cons x nil) > 0) => singleton x
          | (cons x xs) => fun (H : length (cons x xs) > 0) => consNE x
(fromList xs _ )
          end).
  - cbn in H. (* H: 0 > 0 *) exfalso. abstract omega.
  - subst xs. cbn. abstract omega.
Fail Defined.
```

Outch, the last command gave an error message. What was the problem?

The problem is that the function is not guarded, even though all goals
have been solved. (Exercise: Write an unguarded 'proof' for `False`.)
You can use the command `Guarded.` to check if your definition is guarded.

Let's look at the unsuggared version of the term.


```
Set Printing All.
Show Proof.

(fix fromList (l : list A) : forall _ : gt (@length A l) O, nonEmpty A :=
   match l as l0 return (forall _ : gt (@length A l0) O, nonEmpty A) with
   | nil =>
       fun H : gt (@length A (@nil A)) O =>
       False_rect (nonEmpty A) (fromList_subproof H) : nonEmpty A
   | cons x xs =>
       match xs as xs0 return (forall _ : gt (@length A (@cons A x xs0))
O, nonEmpty A) with
       | nil => fun _ : gt (@length A (@cons A x (@nil A))) O =>
@singleton A x
       | cons a l0 =>
           let xs0 : list A := @cons A a l0 in
           fun H : gt (@length A (@cons A x xs0)) O =>
           @consNE A x
             (fromList xs0
                ((fromList_subproof0 x a l0 H : gt (@length A (@cons A a
l0)) O)
                 :
                 gt (@length A xs0) O))
       end
   end)
```

As you can see, the last recursive call is on `xs0`, not `xs`. This is a
common problem if you use the 'complex pattern' syntactic sugar like

```
match l with
| nil => ...
| (cons x nil) => ...
| (cons x xs) => ...
end
```

Instead, it is almost always better (when dealing with dependent types),
to have two nested matches:

```
Fixpoint fromList (l : list A) : length l > 0 -> nonEmpty A.
  refine (match l with
          | nil => fun (H : length nil > 0) => _
          | cons x l' =>
            fun (_ : length (cons x l') > 0) => (* We can already forget
the proof here that [l] is not empty *)
              match l' with
              | nil => singleton x
              | cons y l'' => consNE x (fromList l' _)
              end
          end).
  - cbn in H. (* H: 0 > 0 *) exfalso. abstract omega.
  - (* ??? *)
```

Now, the function is guarded, but we can't prove the second obligation.

See my other mail for the solution for this (using the function
`list_nil_or_not_empty`).