The Coq mailing list

[Maximilian Wuttke <mwuttke97 AT posteo.de>]

Note that even defining `fromList` this way is somewhat complicated. One
possible implementation:

```
  Fixpoint fromList (l : list A) : 1 <= length l -> nonEmpty A.
  Proof.
    destruct l as [ | x l'].
    - intros H. exfalso. cbn in H. abstract omega.
    - destruct l' as [ | y l''] eqn:E.
      + intros _. exact (singleton x).
      + intros H. refine (consNE x (fromList l' _)).
        abstract (subst; cbn in *; omega).
  Defined.
```

Note that this is structurally recursive over the list. In the second
case, we have to make another case distinction on whether the rest of
the list is empty. Note that in the last case, we make recursive use of
`fromList l' _`, not `fromList (cons y l'') _`.

Note that `1 <= length l` is introduced *after* the case distinction on
`l`. This makes sure that `l` is also modified after the case
distinction. This pattern is called the 'convoy pattern', see [1].

[1]: <http://adam.chlipala.net/cpdt/cpdt.pdf>.

On 30/09/2020 20:52, jonikelee AT gmail.com wrote:
> That fixpoint fromList is not going to be structurally recursive as it
> is defined, even if you do solve its remaining subgoals.  I would
> suggest this alternative:
> 
> Fixpoint fromList (l : list A)(lgt0 : length l > 0) :nonEmpty A.
> 
> If you still really need to have a single arg version of fromList that
> takes a sigma type, my suggestion is to define it in terms of the above
> alternative.
> 
> On Wed, 30 Sep 2020 13:21:49 -0500
> Agnishom Chattopadhyay <agnishom AT cmi.ac.in> wrote:
> 
>> I am trying to write a function whose argument type is a sigma type.
>> Here are some details.
>>
>> Inductive nonEmpty (A : Type) : Type :=
>> | singleton : A -> nonEmpty A
>> | consNE : A -> nonEmpty A -> nonEmpty A.
>>
>> Arguments singleton {A}.
>> Arguments consNE {A}.
>>
>> Section NonEmpty.
>>
>>   Variable A : Type.
>>
>>   Fixpoint toList (l : nonEmpty A) :=
>>     match l with
>>     | singleton x => (cons x nil)
>>     | consNE x xs => (cons x (toList xs))
>>     end.
>>
>>   Fixpoint fromList (l : {l : list A | length l > 0}) : nonEmpty A.
>>     refine (match (proj1_sig l) with
>>             | nil => _
>>             | (cons x nil) => singleton x
>>             | (cons x xs) => consNE x (fromList (exist (fun xs =>
>> length xs
>>> 0) xs _))  
>>             end).
>>
>> Now, how do I solve these goals? For the first one, I want to show a
>> contradiction, saying that (proj1_sig l) couldn't have been nil,
>> given that we know that length ((proj1_sig l)) > 0. However, the
>> equation (proj1_sig l) = nil is not present in the context. It is
>> very similar in the case of the other hole as well.
>>
>> --Agnishom
>