coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Houda Anoun <anoun AT labri.fr>
- To: coq-club AT pauillac.inria.fr
- Cc: anoun AT labri.fr
- Subject: [Coq-Club] generic tactic
- Date: Thu, 25 Nov 2004 11:16:08 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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|
==============================
- [Coq-Club] generic tactic, Houda Anoun
- Re: [Coq-Club] generic tactic, casteran
Archive powered by MhonArc 2.6.16.