The Coq mailing list

[Marcus Ramos <mvmramos AT gmail.com>]

Hi Rui,

Thanks for the reply. Here it is. Just try to execute the last line.

-----------------------------------------------------------------

Require Import Ascii.

Require Import String.

Require Import Compare_dec.

Open Scope string_scope.

Definition b0: bool := false.

Definition b1: bool := true.

(* CONVERT ASCII TO STRING *)

Definition chr_to_str (c: ascii): string :=

   match c with

   | Ascii b0 b0 b0 b0 b1 b1 b0 b0  => "0"

   | Ascii b1 b0 b0 b0 b1 b1 b0 b0  => "1"

   | Ascii b0 b1 b0 b0 b1 b1 b0 b0  => "2"

   | Ascii b1 b1 b0 b0 b1 b1 b0 b0  => "3"

   | Ascii b0 b0 b1 b0 b1 b1 b0 b0  => "4"

   | Ascii _  _  _  _  _  _  _  _   => "#"

   end.

Definition nat_to_str (n: nat): string :=

   chr_to_str (ascii_of_nat (n+48)).

(* STATES *)

Definition state: Type := (nat*bool*bool)%type.

(* STATE NAME PRINT*)

Definition state_name_print (n: nat): string :=

"q" ++ nat_to_str n.

(* STATE PRINT *)

Fixpoint state_print (q: state): string :=

   match q with

   | (n,i,f) => state_name_print n

   end.

(* STATE SETS *)

Inductive state_set: Type :=

   | sset_empty: state_set

   | sset_item: state->state_set

   | sset_build: state->state_set->state_set.

(* STATE SET PRINT *)

Fixpoint state_set_print (s: state_set): string :=

   match s with

   | sset_empty => ""

   | sset_item st => "

" ++ state_print st 

   | sset_build st s' => "

" ++ state_print st ++ state_set_print s'

   end.

(* INSERT STATE IN AN ORDERED SET *)

Fixpoint insert_state (q: state)(s: state_set): state_set :=

   match s with

   | sset_empty => sset_item q

   | sset_item q' => match q, q' with

                     | (n,i,f),(n',i',f') => if leb n n' 

                                                then sset_build q (sset_item q')

                                                else sset_build q' (sset_item q)

                     end

   | sset_build q' s' => match q, q' with

                     | (n,i,f),(n',i',f') => if leb n n' 

                                                then sset_build q s

                                                else sset_build q' (insert_state q s')

                         end

   end.

(* SORT STATE SET *)

Fixpoint sort_state_set (s: state_set): state_set :=

   match s with

   | sset_empty => sset_empty

   | sset_item q => s

   | sset_build q s' => insert_state q (sort_state_set s')

   end.

(* BUILD A NUMBER BASED ON THE NUMBERS OF THE STATES IN THE ORDERED STATE SET *)

Fixpoint build_state_number (s: state_set): nat :=

   match s with

   | sset_empty => O

   | sset_item (n,i,f) => n

   | sset_build (n,i,f) s' => (build_state_number s')*10+n

   end.

Definition est0: state := (0,false,false).

Definition est1: state := (1,false,false).

Definition est2: state := (2,false,false).

Definition est3: state := (3,false,false).

Definition est4: state := (4,false,false).

Definition eset: state_set :=

sset_build est4 (

sset_build est3 (

sset_build est2 (

sset_build est1 (

sset_item est0)))).

(* SHOULD PRINT STRING Q4 Q3 Q2 Q1 Q0 *)

Eval compute in state_set_print eset.

(* SHOULD PRINT STRING Q0 Q1 Q2 Q3 Q4 *)

Eval compute in state_set_print (sort_state_set eset).

(* SHOULD PRINT NAT 43210 *)

Eval compute in build_state_number (sort_state_set eset).

-----------------------------------------------------------------

Regards,

Marcus.

2013/8/31 Rui Baptista <rpgcbaptista AT gmail.com>

That is a bug. Maybe if you include more information in some match-with-end pattern, you can get around it. Here are some examples:

(* without wildcards, with as-in-return, type-checks *)
Fixpoint le_pred (n1 n2 : nat) (H1 : n1 <= n2) : pred n1 <= pred n2 :=
  match H1 in _ <= n2 return pred n1 <= pred n2 with
  | le_n      => le_n (pred n1)
  | le_S n2 H1 =>
    match n2 as n2 return pred n1 <= pred n2 -> pred n1 <= pred (S n2) with
    | 0   => fun H2 => H2
    | S n3 => fun H2 => le_S (pred n1) (pred (S n3)) H2
    end (le_pred n1 n2 H1)
  end.

(* without wildcards, without as-in-return, doesn't type-check *)
Fixpoint le_pred (n1 n2 : nat) (H1 : n1 <= n2) : pred n1 <= pred n2 :=
  match H1 with
  | le_n      => le_n (pred n1)
  | le_S n2 H1 =>
    match n2 with
    | 0   => fun H2 => H2
    | S n3 => fun H2 => le_S (pred n1) (pred (S n3)) H2
    end (le_pred n1 n2 H1)
  end.

(* with wildcards, with as-in-return, type-checks *)
Fixpoint le_pred (n1 n2 : nat) (H1 : n1 <= n2) : pred n1 <= pred n2 :=
  match H1 in _ <= n2 return pred n1 <= pred n2 with
  | le_n => le_n _
  | le_S n2 H1 =>
    match n2 as n2 return pred n1 <= pred n2 -> pred n1 <= pred (S n2) with
    | 0 => fun H2 => H2
    | S _ => fun H2 => le_S _ _ H2
    end (le_pred _ _ H1)
  end.

(* with wildcards, without as-in-return, stack-overflows *)
Fixpoint le_pred (n1 n2 : nat) (H1 : n1 <= n2) : pred n1 <= pred n2 :=
  match H1 with
  | le_n => le_n _
  | le_S n2 H1 =>
    match n2 with
    | 0 => fun H2 => H2
    | S _ => fun H2 => le_S _ _ H2
    end (le_pred _ _ H1)
  end.