Bruno Carneiro (Jan 08 2022 at 11:17): Bruno Carneiro (Jan 08 2022 at 11:17):Hi,
Let's say that I have the following:
Inductive tm : Type :=
| tm_const : string -> tm
| tm_var : string -> tm
.
Now, I want to make a new inductive type, with two constructors:
Inductive atom : Type :=
| atom_ground : string -> list tm -> atom
| atom_regular : string -> list tm -> atom
.
However, I want to encode in the constructor, that atom_ground can only yield an atom, IF all terms, in its list of terms, are tm_const,
And that not all terms in atom_regular's list of terms can be tm_const.
Gaëtan Gilbert (Jan 08 2022 at 11:21):(deleted)
Bruno Carneiro (Jan 08 2022 at 11:21):I have updated my question, sorry for my butter fingers :D
Gaëtan Gilbert (Jan 08 2022 at 13:10):something like ?
Require Import List String.
Inductive tm : Type :=
| tm_const : string -> tm
| tm_var : string -> tm
.
Definition is_const t := match t with tm_const _ => True | _ => False end.
Inductive atom : Type :=
| atom_ground : string -> forall l : list tm, Forall is_const l -> atom
| atom_regular : string -> forall l : list tm, not (Forall is_const l) -> atom
.
One suggestion is to make the notions of ground and regular predicates on atom (which itself doesn't distinguish between these states).
Bruno Carneiro (Jan 08 2022 at 13:40):Gaëtan Gilbert said:
something like ?
Require Import List String. Inductive tm : Type := | tm_const : string -> tm | tm_var : string -> tm . Definition is_const t := match t with tm_const _ => True | _ => False end. Inductive atom : Type := | atom_ground : string -> forall l : list tm, Forall is_const l -> atom | atom_regular : string -> forall l : list tm, not (Forall is_const l) -> atom .
If I have the following
Definition eqb_term (lterm : tm) (rterm: tm) : bool :=
match lterm, rterm with
| tm_var _, tm_const _ => false
| tm_const _, tm_var _ => false
| tm_var lvalue, tm_var rvalue => eqb_string lvalue rvalue
| tm_const lvalue, tm_const rvalue => eqb_string lvalue rvalue
end.
Fixpoint eqb_term_list (l1 l2 : list tm) : bool :=
match l1, l2 with
| nil, nil => true
| h :: l, h' :: r => if eqb_term h h' then eqb_term_list l r else false
| _, _ => false
end.
Definition eqb_atom (latom : atom) (ratom : atom) : bool :=
match latom, ratom with
| atom_ground sym l1, atom_ground sym' l2 => if eqb_string sym sym' then eqb_term_list l1 l2 else false
| atom_regular sym l1, atom_regular sym' l2 => if eqb_string sym sym' then eqb_term_list l1 l2 else false
| _, _ => false
end.
Then, it would not be possible to use this function with the inductive atom with the proof in it, right?
If I want to retain computability, how would you go about it?
So far I've come to terms that, the following:
Inductive well_formed : atom -> Prop :=
| well_formed_ground : forall sym l,
Forall is_const l ->
well_formed (atom_ground sym l)
| well_formed_regular : forall sym l,
well_formed (atom_regular sym l)
.
Might be the most sensible approach, given that I want to retain computability.
Gaëtan Gilbert (Jan 08 2022 at 14:39):you can replace the Foralls by forallbs
Definition is_const t := match t with tm_const _ => true | _ => false end.
Inductive atom : Type :=
| atom_ground : string -> forall l : list tm, is_true (forallb is_const l) -> atom
| atom_regular : string -> forall l : list tm, is_true (negb (forallb is_const l)) -> atom
.
is_true has trivial equality
Gaëtan Gilbert (Jan 08 2022 at 14:40):not sure what exactly you mean by computability
Gaëtan Gilbert (Jan 08 2022 at 14:40):the well_formed approach can work well
Paolo Giarrusso (Jan 08 2022 at 15:47):If you're worried about proof equality being uncomputable, you can most likely ignore the proofs (or use is_true's tip by Gaëtan)
Last updated: Oct 13 2024 at 01:02 UTC