The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

> 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