search

gmalecha / HL-Compiler

MIT License
0 stars 1 forks source link

Here's an example of parsing #2

Open gmalecha opened 8 years ago

gmalecha commented 8 years ago 
Require Import Coq.Strings.String.
Require Import Coq.Strings.Ascii.

Local Open Scope string_scope.

Axiom is_T : string -> Prop.

Axiom zero_is_T : is_T "0".
Axiom one_is_T : is_T "1".
Axiom plus_is_T : forall s s',
    is_T s ->
    is_T s' ->
    is_T ("+" ++ s ++ s').
Axiom give_up : forall s, is_T s.

Theorem plus_is_T' : forall s s' s'',
    is_T s' ->
    is_T s'' ->
    s = s' ++ s'' ->
    is_T (String "+" s).
Proof.
  intros. subst.
  apply plus_is_T; auto.
Qed.

Goal is_T "+1+11".
  eapply plus_is_T'.
  apply one_is_T.
  eapply plus_is_T'.
  apply one_is_T.
  apply one_is_T.
  reflexivity. reflexivity.
Qed.