Stream: Coq users

Topic: Simple question about subtyping?


view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Jan 08 2022 at 11:21):

(deleted)

view this post on Zulip Bruno Carneiro (Jan 08 2022 at 11:21):

I have updated my question, sorry for my butter fingers :D

view this post on Zulip 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
.

view this post on Zulip Li-yao (Jan 08 2022 at 13:11):

One suggestion is to make the notions of ground and regular predicates on atom (which itself doesn't distinguish between these states).

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Jan 08 2022 at 14:40):

not sure what exactly you mean by computability

view this post on Zulip Gaëtan Gilbert (Jan 08 2022 at 14:40):

the well_formed approach can work well

view this post on Zulip 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: Feb 06 2023 at 12:04 UTC