The Coq mailing list

[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|
==============================