The Coq mailing list

[Agnishom Chattopadhyay <agnishom AT cmi.ac.in>]

Thank you, Maximilian. I understand that one way to define this function is to define it "as a proof". One reason I try to avoid this is because it sometimes gives me a term which is very difficult to understand and use in later proofs. But I will still try it and see what happens.

As for what jonikelee is saying: Even if I rephrase my definition as:

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.

On Wed, Sep 30, 2020 at 2:19 PM Maximilian Wuttke <mwuttke97 AT posteo.de> wrote:

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
>