The Coq mailing list

[AUGER <Cedric.Auger AT lri.fr>]

Le Wed, 05 May 2010 08:06:02 +0200, geng chen <chengeng4001 AT gmail.com> a  
écrit:

>  Hi everyone,
>   Recently, I need to develop a prototype in Coq. But I've met a  
> problem, it
> seems naive, but it is important for me.
>
> Inductive prim : Set :=
>   A : prim
> | B : prim.
>
> Inductive comp : Set := list all.
>
> Inductive all : Set :=
>   C : prim -> all
> | D : comp -> all.
>
> Is there anyway to define the 3 types aboves? Do I need to use some  
> special
> kinds of method to declare the type "all" in the front of the definition?
>
> Thanks, best regards
> Chen

There are mainly two ways to do this:

"Require Import List.
Inductive prim : Set :=
  A : prim
| B : prim.

(*Inductive comp : Set := list all.*)

Inductive all : Set :=
  C : prim -> all
| D : list all -> all.

Definition comp : Set := list all. (* if you really need it *)"

and

"Require Import List.
Inductive prim : Set :=
  A : prim
| B : prim.

(*Inductive comp : Set := list all.*)

Inductive all : Set :=
  C : prim -> all
| D : comp -> all
with comp : Set :=
| nil_comp : comp
| cons_comp : all -> comp -> comp."

In the first solution, you have access to all List library for comp,
but mutual induction will be harder
(test it, to understand what I mean;
 you can also have a look or Induction Scheme in the Coq reference manual);
in the second case, you have to redefine all what you need on lists,
but mutual induction will be piece of cake.

In both ways, you should really take a look on the manual,
 since induction being central in Coq
 (brief history: Coq is named after CoC= calculus of constructions
  but now uses CIC= calculus of inductive constructions),
 it is rather well explained.

For an example of both uses:


Require Import Bool.
Definition prim_eq (p1 p2: prim): bool :=
 match p1, p2 with
 | A, A => true
 | B, B => true
 | _, _ => false
 end.
Lemma prim_eq_lemma: forall a1 a2, if prim_eq a1 a2 then a1 = a2 else a1  
<> a2.
Proof.
 destruct a1; destruct a2; simpl.
    split.
   intros; discriminate.
  intros; discriminate.
 split.
Qed.

1. boolean equality definition (without using "decide equality"); play  
with uncommenting...
(using Induction Scheme may ease things a lot;
 there may also Coq functionnalities I am not aware of, or powerfull  
tactics,
 but it is always good to do how things are really done)

Definition forallb2 {A: Set} (f: A -> A -> bool): list A -> list A -> bool  
:=
 fix forallb2 (l1 l2: list A) :=
 match l1, l2 with
 | nil, nil => true
 | a1::l1, a2::l2 => f a1 a2 && forallb2 l1 l2
 | _, _ => false
 end.

Fixpoint all_eq (a1 a2: all): bool :=
  match a1, a2 with
  | C p1, C p2 => prim_eq p1 p2
  | D l1, D l2 => forallb2 all_eq l1 l2
  | _, _ => false
  end.
(*
Lemma all_eq_lemma: forall a1 a2, if all_eq a1 a2 then a1 = a2 else a1 <>  
a2.
Proof.
 induction a1; destruct a2; simpl; try (intros; discriminate).
  generalize (prim_eq_lemma p p0); destruct (prim_eq p p0).
   intros H; case H; split.
  intro H; now injection.
 (* now you are stuck *)
 (* but before being really stuck, we can do some cleaning: *)
 cut (if forallb2 all_eq l l0 then l = l0 else l <> l0).
  destruct (forallb2 all_eq l l0).
   intro H; case H; split.
  intro H; now injection.
 (* and start an induction *)
 revert l0; induction l; destruct l0; simpl; try (intros; discriminate).
  split.
 generalize (IHl l0); clear IHl; destruct (forallb2 all_eq l l0); simpl.
  intro H; case H.
Abort.
*)
Lemma comp_eq_lemma:
 (forall a1 a2, if all_eq a1 a2 then a1 = a2 else a1 <> a2) ->
 forall l l0, if forallb2 all_eq l l0 then l = l0 else l <> l0.
Proof.
 intro EQ; induction l; destruct l0; simpl; try (intros; discriminate).
  split.
 generalize (EQ a a0); clear EQ.
 destruct (all_eq a a0); simpl.
  intro H; case H; clear a0 H.
  generalize (IHl l0); clear IHl.
  destruct (forallb2 all_eq l l0).
   intro H; case H; split.
  intro H; now injection.
 intro H; now injection.
(*Qed.*)
Defined.

Lemma all_eq_lemma: forall a1 a2, if all_eq a1 a2 then a1 = a2 else a1 <>  
a2.
Proof.
 fix 1 (* a trick, that makes you lose guardedness *).
(* exact all_eq_lemma.
Qed.*)
 destruct a1; destruct a2; simpl; try (intros; discriminate).
  generalize (prim_eq_lemma p p0); destruct (prim_eq p p0).
   intros H; case H; split.
  intro H; now injection.
 generalize (comp_eq_lemma all_eq_lemma l l0).
 destruct (forallb2 all_eq l l0).
  intro H; case H; split.
 intro H; now injection.
Qed.


2. boolean equality definition (without using "decide equality"); rather  
straightforward

Fixpoint all_eq (a1 a2: all): bool :=
  match a1, a2 with
  | C p1, C p2 => prim_eq p1 p2
  | D l1, D l2 => comp_eq l1 l2
  | _, _ => false
  end
with comp_eq (c1 c2: comp): bool :=
  match c1, c2 with
  | nil_comp, nil_comp => true
  | cons_comp a1 c1, cons_comp a2 c2 => all_eq a1 a2 && comp_eq c1 c2
  | _, _ => false
  end.

Lemma all_eq_lemma: forall a1 a2, if all_eq a1 a2 then a1 = a2 else a1 <>  
a2
with comp_eq_lemma: forall l l0, if comp_eq l l0 then l = l0 else l <> l0.
Proof. (* you also lose guardedness:
 exact all_eq_lemma.
 exact comp_eq_lemma.
Qed. *)
 destruct a1; destruct a2; simpl; try (intros; discriminate).
  generalize (prim_eq_lemma p p0); destruct (prim_eq p p0).
   intros H; case H; split.
  intro H; now injection.
 generalize (comp_eq_lemma c c0).
 destruct (comp_eq c c0).
  intro H; case H; split.
 intro H; now injection.
Proof.
 destruct l; destruct l0; simpl; try (intros; discriminate).
  split.
 generalize (all_eq_lemma a a0).
 destruct (all_eq a a0); simpl.
  intro H; case H; clear a0 H.
  generalize (comp_eq_lemma l l0).
  destruct (comp_eq l l0).
   intro H; case H; split.
  intro H; now injection.
 intro H; now injection.
Qed.



One last thing, you may consider using Type insteal of Set.
It will be less efficient but more flexible.



--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay