The Coq mailing list

[Serge Leblanc <serge.leblanc AT wanadoo.fr>]

Hi,

In the attached file, how can I tell to the function "size" that decrease recursion is done on (snd b0)? 

File "/home/serge/produkto/maŝinlingvo/programoj/gle/zen.v", line 60, characters 2-204
Error:
Recursive definition of size is ill-formed.
In environment
size : trie -> nat
t : trie
b : bool
arcs : PositiveMap.t trie
fold_left : list (positive * trie) -> nat -> nat
l : list (positive * trie)
a0 : nat
b0 : positive * trie
t0 : list (positive * trie)
Recursive call to size has principal argument equal to
"snd b0"
instead of arcs

Thanks,

--
Serge Leblanc
gpg --keyserver hkp://subkeys.pgp.net --recv-keys 0x73791C2B
Fingerprint: 8E0C 0D6D E026 A278 9278 BF4F 1A93 D552 7379 1C2B

Require Import BinPos.
Require Import List.
Require Import FMapPositive.


Section automata.

  (* Simplistic automata from Gérard Huet *)

  Definition letter := positive.
  Definition word := list letter.

  Inductive trie : Set := Trie : bool -> PositiveMap.t trie -> trie.

  Definition empty : trie := Trie false (PositiveMap.empty trie).
  Definition epsilon : trie := Trie true (PositiveMap.empty trie).

  Fixpoint make (w:word){struct w} : trie :=
    match w with
      | nil => Trie true (PositiveMap.empty trie)
      | n :: r => Trie false (PositiveMap.add n 
                    (make r)
                    (PositiveMap.empty trie))
    end.

  Fixpoint mem (w:word)(t:trie){struct w} : bool :=
    match t with
    | Trie b l => match w with
        | nil => b
        | n :: r => match (PositiveMap.find n l) with
              | Some v => mem r v
              | None => false
            end
        end
    end.

  Lemma PositiveMap_find_add : forall (A:Set)(i :positive)(v:A)
    (m:PositiveMap.t A), PositiveMap.find i (PositiveMap.add i v m) = Some v.
  Proof.
    intros.
    apply PositiveMap.find_1.
    apply PositiveMap.add_1.
    apply PositiveMap.E.eq_refl.
  Qed.

  Lemma mem_make : forall w:word, mem w (make w) = true.
  Proof.
    intro.
    induction w.
    simpl in |- *.
    reflexivity.
    simpl in |- *.
    rewrite PositiveMap_find_add in |- *.
    exact IHw.
  Qed.


  Definition dirac (b:bool) := if b then 1%nat else 0%nat.

  Function size (t:trie) : nat := 
    let count _ (t':trie)(n:nat) : nat := plus n (size t') in
      match t with
        | Trie b arcs => plus (PositiveMap.fold count arcs 0%nat) (dirac b)
        end.
      (*where "n + m" := (plus n m).*)

  (*
  Fixpoint size (t:trie){struct t} : nat := 
    match t with
      | Trie b arcs => (PositiveMap.fold count arcs 0%nat) + (dirac b)
      end
    with count _ t n : nat := n + (size t)
    where "n + m" := (plus n m).
  *)


(*Let saluton := 19::1::12::21::20::15::14::nil.*)

(*
  Fixpoint creat_from_list (l:list (letter * letter)){struct l} :=
    match l with
    | nil => Trie false (PositiveMap.empty trie)
    | (a,b)::t => 
    
*)

Attachment: signature.asc
Description: This is a digitally signed message part