The Coq mailing list

[e+coq-club AT x80.org (Emilio Jesús Gallego Arias)]

Hi Ilmārs,

there's two kind of standard workarounds to this problem (apart from
making proofs transparent and being smarter in definitions). Both of
them involve changing your list definition:

- Use list T n ≡ { s : list T | length s = n }

  You'll also need to prove proof irrelevance on the proof, so it is a
  good idea to use decidable predicates, see ssreflect tuple.v for an
  example of this.

- Use list T n := fix V n := match n with | 0 => unit | S n => T * V n

Hope it helps.
E.

Ilmārs Cīrulis 
<ilmars.cirulis AT gmail.com>
 writes:

>> Can you give some code here please? I don't see what transparency can
> help here.
>
> Pierre, here is a code example.
>
> ===
> Require Import Utf8 Arith.
> Set Implicit Arguments.
>
> Inductive list A: nat → Type :=
>  | nil: list A 0
>  | cons: ∀ n, A → list A n → list A (S n).
>
> Arguments nil [A].
> Infix "::" := cons (at level 60, right associativity).
>
> Fixpoint app A n m (L: list A n) (L0: list A m): list A (n + m) :=
>  match L with
>  | nil => L0
>  | a :: t => a :: app t L0
>  end.
>
> Infix "++" := app (at level 60, right associativity).
>
> Definition add_to_end A n (L: list A n) (x: A): list A (S n) :=
>  eq_rect _ _ (L ++ x :: nil) _ ltac:(rewrite plus_comm, plus_n_O; auto).
>
> Eval compute in (add_to_end nil 1).
>
> (*
>      = match
>          match
>            match Nat.add_comm 0 1 in (_ = y) return (y = 1) with
>            | eq_refl => eq_refl
>            end in (_ = y) return (y = 1)
>          with
>          | eq_refl =>
>              match match plus_n_O 1 in (_ = y) return (y = 1) with
>                    | eq_refl => eq_refl
>                    end in (_ = y) return (1 = y) with
>              | eq_refl => plus_n_O 1
>              end
>          end in (_ = y) return (list nat y)
>        with
>        | eq_refl => 1 :: nil
>        end
>      : list nat 1
> *)
> ===
>
>> If the inductive proof of n + 1 = S n is Qeded, then you cannot reduce it
> in proof terms using it, I think that's what Ilmārs is saying. There's
> currently no getting around reproving it transparently.
>
> Matthie, it must be this.
> I'm using Coq for fun and experience, so learning vocabulary and theory
> isn't in the first place. Probably not for good.
>
>
> ---
> Thank you.
>
> On Fri, Apr 22, 2016 at 2:59 PM, Matthieu Sozeau 
> <mattam AT mattam.org>
>  wrote:
>
>> If the inductive proof of n + 1 = S n is Qeded, then you cannot reduce it
>> in proof terms using it, I think that's what Ilmārs is saying. There's
>> currently no getting around reproving it transparently.
>> -- Matthieu
>>
>> Le ven. 22 avr. 2016 à 13:55, Pierre Courtieu 
>> <pierre.courtieu AT gmail.com>
>> a écrit :
>>
>>> 2016-04-22 0:32 GMT+02:00 Ilmārs Cīrulis 
>>> <ilmars.cirulis AT gmail.com>:
>>> > Probably I can't. They're opaque and that's all.
>>>
>>> I am afraid so.
>>>
>>> > I need them, for example, to prove that types list A (n + 1) and list A
>>> (S
>>> > n) are equal and then use this equality in computations.
>>>
>>> I don't understand, an equality cannot help "computation" as far as I
>>> can tell. You mean that this equality allows to rewrite *and then* you
>>> can compute right? But then the transparency is not the problem.
>>>
>>> > For now I just prove necessary equality again, this time transparently.
>>>
>>> Can you give some code here please? I don't see what transparency can
>>> help here.
>>>
>>> Best
>>> Pierre Courtieu
>>>
>>