CODEWITHSUNDEEP
coqparser-combinators
Kijeong Lim
Kijeong Lim

Reputation: 133

To prove the unfolding lemma for `some`

Require Import Arith.
Require Import Ascii.
Require Import Coq.Arith.PeanoNat.
Require Import Coq.Lists.List.
Require Import Coq.Program.Program.
Require Import Coq.Strings.Byte.
Require Import Coq.Strings.String.

Import ListNotations.

Definition parser (A : Type) : Type := string -> option (A * string).

Definition isLt {A : Type} (p : parser A) : Prop :=
  forall s : string,
  match p s with
  | None => True
  | Some (x, s') => length s' < length s
  end.

#[program]
Fixpoint some {A : Type} (p1 : parser A) (p1_isLt : isLt p1) (s : string) {measure (length s)} : option (list A * string) :=
  match p1 s with
  | None => None
  | Some (x, s') =>
    match some p1 p1_isLt s' with
    | None => Some ([x], s')
    | Some (xs, s'') => Some (x :: xs, s'')
    end
  end.
Next Obligation. pose proof (p1_isLt s) as H. rewrite <- Heq_anonymous in H. assumption. Defined.

Lemma some_unfold {A : Type} (p1 : parser A) (p1_isLt : isLt p1) (s : string) :
  some p1 p1_isLt s =
  match p1 s with
  | None => None
  | Some (x, s') =>
    match some p1 p1_isLt s' with
    | None => Some ([x], s')
    | Some (xs, s'') => Some (x :: xs, s'')
    end
  end.
Proof.
  unfold some at 1. unfold some_func. rewrite fix_sub_eq.
  { destruct (p s) as [[x s'] | ] eqn: OBS_p_s; simpl.
    - rewrite OBS_p_s. destruct (some p p_isLt s') as [[xs s''] | ] eqn: OBS_some_p_s'.
      + unfold some in OBS_some_p_s'. unfold some_func in OBS_some_p_s'.
        rewrite OBS_some_p_s'. reflexivity.
      + unfold some in OBS_some_p_s'. unfold some_func in OBS_some_p_s'.
        rewrite OBS_some_p_s'. reflexivity.
    - rewrite OBS_p_s. reflexivity.
  }
  { intros [_A [_p [_p_isLt _s]]] f g f_eq_g; simpl.
    admit. (* because `destruct (_p _s).` fails *)
  }
Admitted.

How can I prove the lemma some_unfold?

I proved an unfold lemma for other program fixpoint:

  1. unfold the program fixpoint.
  2. rewrite fix_sub_eq.
  3. - destruct the argument which has measure; eauto.
  4. - intros. destruct the argument again; simpl; eauto. rewrite H; eauto. But this problem is slightly different from the above.

Upvotes: 0

Views: 77

Answers (1)

Kijeong Lim
Kijeong Lim

Reputation: 133

Require Import Coq.Program.Wf.

Lemma some_unfold {A : Type} (p1 : parser A) (p1_isLt : isLt p1) (s : string) :
  some p1 p1_isLt s =
  match p1 s with
  | None => None
  | Some (x, s') =>
    match some p1 p1_isLt s' with
    | None => Some ([x], s')
    | Some (xs, s'') => Some (x :: xs, s'')
    end
  end.
Proof.
  unfold some at 1. unfold some_func. rewrite WfExtensionality.fix_sub_eq_ext.
  destruct (p s) as [[x s'] | ] eqn: OBS_p_s; simpl.
  - rewrite OBS_p_s. destruct (some p p_isLt s') as [[xs s''] | ] eqn: OBS_some_p_s'.
    + unfold some in OBS_some_p_s'. unfold some_func in OBS_some_p_s'.
      rewrite OBS_some_p_s'. reflexivity.
    + unfold some in OBS_some_p_s'. unfold some_func in OBS_some_p_s'.
      rewrite OBS_some_p_s'. reflexivity.
  - rewrite OBS_p_s. reflexivity.
Qed.

Upvotes: 0

Related Questions