The Coq mailing list

[gbush <gbush AT mysck.com>]

Hello,

I've been experimenting with a proof of a simple parser that I want to
extract into a nice program.  I can complete the proof using well-founded
induction on the length of the string being parsed, but the proof extracts
to something like...

let rec parse x =
   func x (fun y _ -> parse y).

... which is not very satisfying from my perspective.

So I would like to try to manually eliminate an ad-hoc predicate instead. 
I've had success with this approach with a simpler problem.  However, I am
stuck here.  I've been trying to distill the problem down to its most basic
component, and I think if I had a solution to the following problem, I could
derive a solution to my problem...

Given the following definitions....

(* Terms consist of a single atomic term, and terms formed by binary
operation Imp *)

Inductive Term : Set :=
| Atom : Term
| Imp : Term -> Term -> Term.

(* There are two tokens : one for the atom and one for the imp operator. *)

Inductive Token : Set := AtomToken | ImpToken.

... what should my accessibility predicate (H : ???) look like here so that
I can invert it properly in (parse xs _) and (parse s' _)?

(* The parse function attempts to parse the head of a list of tokens.  If it
can be parsed (polish notation), it returns the parsed term and 
   the remainder of the unparsed list.  If it can not be parsed, it returns
None. *)

Fixpoint parse (s : list Token) (H : _) {struct H} : option (Term * list
Token) :=
match s with
| nil => None
| x :: xs => match x with
   | AtomToken => Some (Atom, xs)
   | ImpToken => match (parse xs _) with
      | None => None
      | Some p => let (P, s') := p in match (parse s' _) with (* Not
structurally recursive on s! *)
         | None => None
         | Some q => let (Q, s'') := q in Some (Imp P Q, s'')
         end
      end
   end
end.

The candidates that I have come up with so far I could not figure out how to
invert without Coq no longer recognizing them as subterms of H when I get to
(parse s' _).  I'm hoping someone can give me some guidance!

Thanks,
Greg

-- 
View this message in context: 
http://www.nabble.com/Accessibility-Predicate-in-Simple-Parser-tf4844960.html#a13861787
Sent from the Coq mailing list archive at Nabble.com.