coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Micaela Mayero <mayero>
Date: Tue, 3 Jul 2001 14:40:21 +0200 (MET DST)

2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id TAA06914 for
<coq-club AT pauillac.inria.fr>;
Mon, 2 Jul 2001 19:37:04 +0200 (MET DST)
Received: from ext.lri.fr (ext.lri.fr [129.175.15.4])
 by nez-perce.inria.fr (8.11.1/8.10.0) with ESMTP id f62Hb3j13144
 for
<coq-club AT pauillac.inria.fr>;
Mon, 2 Jul 2001 19:37:03 +0200 (MET DST)
Received: from sun-demons.lri.fr (sun-demons [129.175.8.90])
 by ext.lri.fr (8.11.1/jtpda-5.3.2) with ESMTP id f62Hb3512956
 ; Mon, 2 Jul 2001 19:37:03 +0200 (MET DST)
Received: from
(paulin@localhost)
 by sun-demons.lri.fr (8.9.3/jtpda-5.3.2) id TAA26550
 ; Mon, 2 Jul 2001 19:37:02 +0200 (MET DST)
X-Authentication-Warning: sun-demons.lri.fr: paulin set sender to
paulin@sun-demons
using -f
From: Christine Paulin
<Christine.Paulin AT lri.fr>
MIME-Version: 1.0
Content-Type: text/plain; charset=iso-8859-1
Content-Transfer-Encoding: 8bit
Message-ID:
<15168.45374.377151.94324 AT gargle.gargle.HOWL>
Date: Mon, 2 Jul 2001 19:37:02 +0200
To: Boite Olivier
<boite AT cnam.fr>
Cc:
coq-club AT pauillac.inria.fr
Subject: Re: delta-reduction and Cases elimination
In-Reply-To:
<3B4048CA.EFF7B8DA AT cnam.fr>
References:
<3B4048CA.EFF7B8DA AT cnam.fr>
X-Mailer: VM 6.90 under Emacs 20.7.1
Reply-To:
Christine.Paulin AT lri.fr
(Christine Paulin)

The problem is that f=g is only provable when f and g are
intensionally equal.

Intensionally equal means they behave exactly the same, in particular
 (f x)=(g x) for x a variable

But it is not true that
 Cases (eq_A_dec a a') of
 (left _) => (f a)
 | (right _) => (f a')
 end
is the same as (f a') when a' is a variable

What is possible is to prove
 (a':A)Cases (eq_A_dec a a') of
 (left _) => (f a)
 | (right _) => (f a')
 end = (f a')
It is enough to do Intro; Case (eq_A_dec a a').
The case a=a' |- (f a)=(f a') is solved using a Rewrite
The other one is trivial.

But it only means that f and [a':A]Cases (eq_A_dec a a') of
 (left _) => (f a)
 | (right _) => (f a')
 end
are extensionnally equal (the two functions can be proved to have the
 same output on the same input).

To make a simpler analogy compare the programs
p1 == if x = 0 then 0 else x
p2 == x
p1 and p2 are equivalent because they have the same input/output
behavior but they do not strictly correspond to the same algorithm
and consequentely are not intensionnally equal.

Christine Paulin

Boite Olivier writes:
> hello,
>
> In the following example,
>
> A : Set
> B : Set
> a : A
> f : A->B
> ============================
> f
> =([a':A]
> Cases (eq_A_dec a a') of
> (left _) => (f a)
> | (right _) => (f a')
> end)
>
> where eq_A_dec is (x,y:A){x=y}+{~x=y},
>
> I'd like to perform a delta-reduction, but a'
> would be free in the context.
> How to eliminate the Cases in the abstraction ?
>
>
>
> Best regards
>
> --
> Olivier Boite | (33)1 69 36 73 23
> CNAM Departement d'informatique |
> boite AT cnam.fr
> CEDRIC-IIE, 18 allee J.Rostand 91025 EVRY |
>
>
> <!doctype html public "-//w3c//dtd html 4.0 transitional//en">
> <html>
> hello,
> In the following example,
>   A : Set
>    B : Set
>    a : A
>    f : A->B
>    ============================

[no subject], Micaela Mayero