The Coq mailing list

[Maximilian Wuttke <s8mawutt AT stud.uni-saarland.de>]

In the code, you use syntactic suggar for `match`. Actually, you do two
matches: in the first match, you match for the head-constructor of the
list. In the cons case, you do a second match on the tail. After this,
Coq doesn't know that `(consq _ x2 y)` is "smaller" than the original
list, because it doesn't know that `(consq _ x2 y)` is tail of the
original list. This is why Coq complains about ungarded recursion. What
you want to do is to call `last` on the "syntactical" tail of the
recursive list. We use two nested `match`s to do this:

```
Fail Fixpoint last (A:Set) (s:queue A) {struct s} :
  (not (eq s (nilq A))) -> A:=
  match s with
  | nilq _ => (fun p =>
                (False_elim A (p (eq_refl _))))
  | consq _ x s' =>
    match s' with
    | nilq _ => (fun p => x)
    | (consq _ x2 y) => (fun p => @last A s' _)
    end
  end.
(* Cannot infer this placeholder of type
"s' <> nilq A" in environment:
last : forall (A : Set) (s : queue A), s <> nilq A -> A
A : Set
s : queue A
x : A
s' : queue A
x2 : A
y : queue A
p : consq A x (consq A x2 y) <> nilq A
*)
```

We called `last` on `s'` and Coq knows that `s'` is the tail of the
original list `s`. So the problem of ungarded recursion is solved now.
However, we can't solve the obligation any more. To fix this, we use the
"convoy pattern" once more, and essentially do what the ltac `destruct
s' as [ | x2 s'']` would do:

```
Theorem not_eq_consq_nilq' (A:Set)(x:A) (s:queue A) (y:queue A) :
eq s (consq A x y) ->
not (eq s (nilq A)).
intro.
Proof.
  congruence.
Qed.

Fixpoint last (A:Set) (s:queue A) {struct s} :
  (not (eq s (nilq A))) -> A:=
  match s with
  | nilq _ => (fun p =>
                (False_elim A (p (eq_refl _))))
  | consq _ x s' =>
    match s' as s0' return (s' = s0' -> _)  with
    | nilq _ => (fun p p' => x)
    | (consq _ x2 s'') =>
      (fun Eqn p => @last A s' (@not_eq_consq_nilq' A x2 s' s'' Eqn))
    end eq_refl
  end.

Compute @last _ (consq _ 4 (consq _ 8 (consq _ 15 (consq _ 16 (consq _
23 (consq _ 42 (nilq _))))))) _.
(* computes 42 *)
```

In the second `match` case, you now get a hypothesis `Eqn : s' = consq A
x2 s'`. This can be used to prove `s' <> nil`. I hope that helped.

Sincerely
Maximilian


On 28/03/2019 23:49, 
psperatto AT gmail.com
 wrote:
>  
> 
> I have defined a set of queues of type A
> and other functions as follows:
> 
>  
> 
> Inductive queue (A:Set):Set :=
> | nilq  : queue A
> | consq : A-> queue A-> queue A.
> 
>  
> 
> Fixpoint ins_back (A:Set)(a:A)(s:queue A):
> (queue A):=
> match s with
> | nilq _ => consq _ a (nilq _)
> | consq _ x y => consq _ x (ins_back _ a y)
> end.
> 
>  
> 
> Theorem False_elim (A:Set)(f:False):A.
> elim f.
> Qed.
> 
> Fixpoint set_queue (A:Set)(s:queue A): Prop:=
> match s with
> | nilq _ => False
> | consq _ x y => True
> end.
> 
> 
> Theorem eq_subst (A:Set)(x y :A)(P:A->Prop)
> (e:(eq x y))(i:(P y)) : P x.
> rewrite -> e.
> exact i.
> Qed.
> 
>  
> 
> Theorem not_eq_consq_nilq (A:Set)(x:A)
> (y:queue A): not (eq (consq A x y)(nilq A)).
> intro.
> exact (eq_subst (queue A) (nilq A)
>       (consq A x y)(set_queue A)
>        (eq_sym H) I).
> Qed.
> 
>  
> 
> I want to define a recursive function that
> computes the last element on a non-empty
> queue.
> 
> To this end I've defined:
> 
>  
> 
> Fixpoint last (A:Set)(s:queue A):
> (not (eq s (nilq A))) -> A:=
> match s with
> | nilq _ => (fun p =>
> (False_elim A (p (eq_refl _))))
> | consq _ x (nilq _) => (fun p => x)
> | consq _ x (consq _ x2 y) =>
> (fun p => last _ (consq _ x2 y)
> (not_eq_consq_nilq _ x2 y))
> end.
> 
>  
> 
> I get the message:
> Cannot guess decreasing argument of fix.
> 
>  
> 
> I don't understand how is defined the order
> relation in Fixpoint definitions. The
> recursive call is in a smaller argument.
> 
>  
> 
> Someone can help me ???
> 
> Regards,
> Patricia
> 
>  
> 
> 
> 
> ------------------------------------------------------------------------
> Avast logo <https://www.avast.com/antivirus>  
> 
> El software de antivirus Avast ha analizado este correo electrónico en
> busca de virus.
> www.avast.com <https://www.avast.com/antivirus>
> 
> 
> <#DAB4FAD8-2DD7-40BB-A1B8-4E2AA1F9FDF2>

Attachment: signature.asc
Description: OpenPGP digital signature