The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Hi Agnishom,

Unfortunately, I don't have a complete solution for your problem because I hit a bug in Coq's implementation so I need to figure out a workaround.  I have rewritten your function, which avoids 'Program' and 'Function', and it generates 7 subgoals. If you can write a transparent proof --closed by Defined-- of these 7 subgoals then I believe  'simpl' would work.

Best,

Mukesh

 

Definition all_parse_trees : 
  list A -> nat ->  Regex * nat -> list parse_tree.
Proof.
  intros w start rn.
  cut (Acc (slexprod _ _ regex_struct lt) rn).
  intros Hacc.
  revert start w. (* arugments are chaned a bit *)
  revert dependent rn.
  refine
    (fix Fn rn Hacc {struct Hacc} := _).
  refine 
    (match rn as rn' return rn = rn' -> _ with 
    | (Epsilon, _) => fun _ _ _  => [parse_epsilon]
    | (CharClass p, _) => fun Ha start w => 
      match nth_error w start with
      | Some a => if p a then [parse_charclass] else []
      | None => []
      end
    | (r1 · r2, len) => fun Ha start w => 
      Fn (r1, len) _ start w >>= fun t1 =>
        map (fun t2 => parse_concat t1 t2) 
        (Fn (r2, (len - parse_length t1)) _ 
        (start + parse_length t1) w)
    | (r1 ∪ r2, len) => fun Ha start w => 
      map (fun t => parse_union_l t) (Fn (r1, len) _ start w) ++
      map (fun t => parse_union_r t) (Fn (r2, len) _ start w)
    | ((r *), len) => fun Ha start w => 
      match len with
      | 0 => [parse_star_nil]
      | _ => 
      (Fn (r, len) _ start w >>= fun t1 =>
        match parse_length t1 with 
        | 0 => []
        | l1 => map (fun t2 => parse_star_cons t1 t2)  
          (Fn (r *, (len - l1)) _ (start + parse_length t1) w)
          ++ [parse_star_nil] end)
      end
    end eq_refl); subst.
    Guarded.
    (* The condition holds up to here *) 
    +
      eapply wf_slexprod.
      Guarded.
      (* 
      Error: <in exception printer>: Anomaly "Uncaught exception Not_found."
      Please report at http://coq.inria.fr/bugs/.
      <original exception>: Uncaught exception Type_errors.TypeError(_, _).
      *)


1/7
Acc (slexprod Regex nat regex_struct lt) (r2, len - parse_length t1)
2/7
Acc (slexprod Regex nat regex_struct lt) (r1, len)
3/7
Acc (slexprod Regex nat regex_struct lt) (r1, len)
4/7
Acc (slexprod Regex nat regex_struct lt) (r2, len)
5/7
Acc (slexprod Regex nat regex_struct lt) (r *, len - l1)
6/7
Acc (slexprod Regex nat regex_struct lt) (r, len)
7/7
Acc (slexprod Regex nat regex_struct lt) rn

On Sat, Sep 2, 2023 at 2:27 AM Agnishom Chattopadhyay <agnishom AT cmi.ac.in> wrote:

Hi all;

I have a function I am trying to define whose well-foundedness is not obvious. I am trying to do it in two different ways: (1) using Program Fixpoint and (2) using Function. In both cases, I am using the fixannot {wf ...}

However,

(1) When I try Program Fixpoint, the function can be defined. But it is opaque to `simpl`. How do I get around this? I need to be able to prove things about this function.

(2) When I use Function, I am getting a strange error message. The error message is not helpful because it references some variable names which I have not used.

Here is the Coq code: https://gist.github.com/Agnishom/1150d29732a6c727396fb6c118dbf375

Any help with this would be appreciated. I originally posted this on StackExchange, but I am corssposting here because I think this would be better suited for a threaded discussion rather than a Q/A style one.

Thanks!

--Agnishom