The Coq mailing list

[casteran AT labri.fr]

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.