Ssreflect Users Discussion List

[Assia Mahboubi <>]

Hello Nada,

  by the way, do not hesitate to ask further questions on coq's zulip 
chat, in the math-comp dedicated stream. It is the best forum for 
getting help and feedback, and for discussing with other users.

https://coq.zulipchat.com

Best wishes,

assia

Le 06/05/2021 à 01:31, Nada Amin a écrit :
> Hi,
>
> I am new to SSReflect. Sorry for the beginner question, I couldn't 
> find a prior answer.
>
> I am using the reglang library:
> https://github.com/coq-community/reglang 
> <https://github.com/coq-community/reglang>
>
> I would like to compute concretely with a regular expression. Here is 
> my attempt:
>
> From mathcomp Require Import all_ssreflect.
> From RegLang Require Import regexp.
> Require Import List.
> Import ListNotations.
> Example simpl_accepts: [false; true] \in Conc (Atom false) (Atom true).
> Proof.
>   compute. rewrite unlock.
>   compute. rewrite unlock.
>   compute.
>   replace (@idP true) with (ssrbool.ReflectT true is_true_true).
>   reflexivity.
>   (* need to show:
>      ReflectT true is_true_true = idP *)
> Admitted.
>
> If only we could show that the replacement is valid, then the proof 
> goes through. But the term idP is opaque. So how does one go about 
> computing with/reasoning about such terms in SSReflect?
>
> Thank you Best wishes, ~n