coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: casteran AT labri.fr
- To: anoun AT labri.fr
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] generic tactic
- Date: Thu, 25 Nov 2004 11:53:06 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hi Houda,
There is something about that in the FAQ (questions 39, 40, and 135, 136).
(proofs of unicity of proofs on a set with decidable equality).
Pierre
Selon Houda Anoun
<anoun AT labri.fr>:
> Hello everybody,
>
> Let's look at the following example:
>
> Require Export Arith.
> Parameter A:Set.
> Parameter eqdecA:forall (a b:A), {a=b}+{a<>b}.
>
> (* inductive definition of binary tree*)
> Inductive tree:Set:=
> leaf:nat->tree
> |node:A->tree->tree->tree.
>
>
> Fixpoint access (tr1 tr2:tree)(n:nat){struct tr1}:(option tree):=
> match tr1 with
> |leaf k=> match (eq_nat_dec k n) with
> |left _ => Some tr2
> |right _ => None
> end
> |node i t1 t2 => match tr2 with
> |node j t1' t2'=>match (eqdecA i j)with
> |left _ => match (access t1 t1' n) with
> |Some ttt => match (access t2 t2' n) with
> |None =>Some ttt
> |Some _ =>None
> end
> |None => (access t2 t2' n)
> end
> |right _=> None
> end
> |leaf _ => None
> end
> end.
>
> The partial recursive function (access) takes two trees as arguments
> (tr1 and tr2) and a number n,
> it returns when it's possible a sub-tree of tr2 which has the same path
> from the root as
> the path of the leaf 'n ' in tr1, so the conditions bellow should be
> verified:
> - tr1 and tr2 should have the same shape
> - there exists only one leaf in tr1 whose number is n
>
> I want to define a generic tactic which proofs some rewriting lemmas
> likes the following:
> /
> Lemma rewr1:forall n , access (node n (node n (leaf 1) (leaf 2)) (leaf
> 3)) (node n (node n (leaf 3) (leaf 1)) (leaf 2)) 1
> =Some(leaf 3)./
> /Lemma rewr2:forall (n m:A) , access (node n (node m (leaf 1) (leaf 2))
> (leaf 3)) (node n (node m (leaf 3) (leaf 1)) (leaf 2)) 1
> =Some(leaf 3)./
>
> The problem comes from the expressions (eqdecA x x) which appear in the
> goal (after simplification by simpl)
> and which should be destructed.
>
> The only idea I found to solve this problem works only if we consider
> the axiom of proof irrelevance in Prop:
> /Axiom proof_irrelevance:forall (A :Prop)(a b:A), a=b./
>
> In fact in that case, we are able to proof easily the following
> rewriting lemma:
> /Lemma eqdec_rw:forall (a:A), eqdecA a a=left (a<>a) (refl_equal a)./
>
> and save this lemma in a data base used with autorewrite (Hint Rewrite
> eqdec_rw:rw.)
> Thus the following tactic works without problem:
> /Ltac rewrite_all:=intros; simpl;autorewrite with rw;auto./
>
> Example:
> /Lemma rewr1:forall n , access (node n (node n (leaf 1) (leaf 2)) (leaf
> 3)) (node n (node n (leaf 3) (leaf 1)) (leaf 2)) 1
> =Some(leaf 3)./
> rewrite_all.
> Qed.
>
> Is it possible to define a generic tactic to solve such rewriting lemmas
> without considering the axiom of proof irrelevance in Prop??
> Thanks in advance for your help
>
> Houda
>
>
> --
> ==============================
> | /\ Houda ANOUN /\ |
> | - LaBRI - |
> | 351 Cours de la libération |
> | 33405 Talence |
> |phone : 0540002489 |
> |e-mail :
>Â anoun AT labri.fr
> |
> |web : www.labri.fr/~anoun|
> ==============================
>
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
> http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>
----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.
- [Coq-Club] generic tactic, Houda Anoun
- Re: [Coq-Club] generic tactic, casteran
Archive powered by MhonArc 2.6.16.