Lessness (Aug 13 2022 at 14:51): Lessness (Aug 13 2022 at 14:51):Hello! I'm trying to write decoding function by myself, by looking at my attempts to decode by hand, but my brain rejects any serious requests today...
If you could direct me - give me keywords or something similar to google and read about - I would be very grateful. Probably something to do with stacks (I have some vague memories of them...).
Set Implicit Arguments.
Structure Language F R := {
function_arity: F -> nat;
relation_arity: R -> nat
}.
Inductive Term F R V (L: Language F R): nat -> Type :=
| variable: V -> Term V L 0
| function_term: forall f, Term V L (function_arity L f)
| apply_function_term: forall n, Term V L (S n) -> Term V L 0 -> Term V L n.
Fixpoint encode_Term F R V (L: Language F R) n (T: Term V L n): list (F + V) :=
match T with
| variable _ v => inr v :: nil
| function_term _ _ f => inl f :: nil
| apply_function_term T1 T0 => encode_Term T1 ++ encode_Term T0
end.
Definition decode_Term F R V (L: Language F R) (x: list (F + V)): option { n & Term V L n }.
Proof.
Admitted.
Made something stack-like. Now to debugging - by trying to prove correctness.
Huỳnh Trần Khanh (Aug 14 2022 at 06:25):Nice. If you need assistance, please let us know!
Lessness (Aug 15 2022 at 12:47):It seems I do.
1) The first question is - is there a simpler/better way to define Term_recursion?
2) The decode_preTerm function seems to be working correctly (as far as I tested), but the proof of this has been stuck. Sooner or later I will find a way, but if someone wants to help, I will be grateful.
Here's the code (about 100 lines). As one can see, I have changed definition of Term (based on the suggestion of Pierre Castéran).
Require Import Utf8 List Lia Arith.
Set Implicit Arguments.
Inductive hlist A (F: A → Type): list A → Type :=
| Hnil: hlist F nil
| Hcons: ∀ x v, F x → hlist F v → hlist F (@cons _ x v).
Structure Language F R := {
function_arity: F → nat;
relation_arity: R → nat
}.
Inductive preTerm F R V (L: Language F R): Type :=
| variable: V → preTerm V L
| function_term: ∀ (f: F), list (preTerm V L) → preTerm V L.
Arguments variable {_} {_} {_} {L}. (*?*)
Definition preTerm_induction F R V (L: Language F R) (P: preTerm V L → Prop):
(∀ (s: V), P (variable s)) →
(∀ (f: F) (v: list (preTerm V L)), Forall P v → P (function_term f v)) →
∀ T, P T.
Proof.
intros H H0. refine (fix IHt (t: preTerm V L) := match t with variable v => H v | function_term f T => _ end).
refine (H0 _ T _). induction T; constructor; auto.
Defined.
Definition preTerm_recursion F R V (L: Language F R) (P: preTerm V L → Type):
(∀ v: V, P (variable v)) →
(∀ (f: F) (v: list (preTerm V L)), hlist P v → P (function_term f v)) →
∀ t, P t.
Proof.
intros H H0. refine (fix IHt (t: preTerm V L) := match t with variable v => H v | function_term f T => _ end).
refine (H0 _ T _). induction T.
+ constructor.
+ constructor. apply IHt. exact IHT.
Defined.
Definition term_correct F R V (L: Language F R) (T: preTerm V L): bool.
Proof.
induction T using preTerm_recursion.
+ exact true.
+ refine (andb (if Nat.eq_dec (length v) (function_arity L f) then true else false) _).
induction X. exact true. exact (andb IHX f0).
Defined.
Definition Term F R V (L: Language F R) := { T: preTerm V L | term_correct T = true }.
Coercion Term_proj1 F R V (L: Language F R) (T: Term V L) := proj1_sig T.
Definition encode_preTerm F R V (L: Language F R) (T: preTerm V L): list (F + V).
Proof.
induction T using preTerm_recursion; simpl in *.
+ exact (inr v :: nil).
+ refine (inl f :: _). induction X.
- exact nil.
- exact (f0 ++ IHX).
Defined.
Definition preterm_free_variables F R V (L: Language F R) (T: preTerm V L): nat :=
match T with
| variable v => 0
| function_term f x => function_arity L f - length x
end.
Definition decode_preTerm_aux F R V (L: Language F R) (T: preTerm V L) (x: list (preTerm V L)): list (preTerm V L).
Proof.
revert T. induction x as [|x t]; intros.
+ exact (T :: nil).
+ remember (preterm_free_variables T) as W. destruct W.
- destruct x.
* exact nil.
* exact (IHt (function_term f (l ++ T :: nil))).
- exact (T :: x :: t).
Defined.
Definition decode_preTerm_step F R V (L: Language F R) (t: list (preTerm V L)) (x: F + V): list (preTerm V L).
Proof.
destruct x.
+ exact (decode_preTerm_aux (function_term f nil) t).
+ exact (decode_preTerm_aux (variable v) t).
Defined.
Definition decode_preTerm F R V (L: Language F R) (x: list (F + V)) :=
fold_left (@decode_preTerm_step F R V L) x nil.
Theorem decode_encode_thm F R V (L: Language F R) (T: Term V L): decode_preTerm L (encode_preTerm T) = Term_proj1 T :: nil.
Proof.
destruct T as [T H]. induction T using preTerm_induction.
+ compute. auto.
+ simpl in *. apply andb_prop in H. destruct H. destruct Nat.eq_dec.
- admit.
Admitted.
Hi,
It may be useful to simplify the definitions as much as possible (especially in the presence of dependent types).
In the code below I used mutually dependent types but it surely could be adapted to lists of preterms.
Inside the section, I dont't have to care about all those arguments.
Section Def.
Variables F V R : Type.
Variable L : Language F R .
Inductive preTerm : Type :=
| variable: V → preTerm
| function_term: F -> preTerms → preTerm
with preTerms : Type :=
preNil : preTerms
| preCons : preTerm -> preTerms -> preTerms.
Scheme preTerm_rect2 := Induction for preTerm Sort Type
with preTerms_rect2 := Induction for preTerms Sort Type.
Fixpoint terms_length (ts : preTerms) : nat :=
match ts with
preNil => 0
| preCons t ts => S (terms_length ts)
end.
Fixpoint preterm_ok (t: preTerm): bool :=
match t with
variable v => true
| function_term f ts => if Nat.eq_dec (function_arity L) (terms_length ts)
then preterms_ok ts
else false
end
with preterms_ok ts :=
match ts with
preNil => true
| preCons t ts => andb (preterm_ok t) (preterms_ok ts)
end.
Fixpoint preterm_2_list (t: preTerm) : list (F + V) :=
match t with
variable v => inr v:: nil
| function_term f ts => inl f :: preterms_2_list ts
end
with
preterms_2_list ts :=
match ts with
preNil => nil
| preCons t ts => preterm_2_list t ++ preterms_2_list ts
end.
End Def.
About decoding: Is the idea you implement as below ?
You decode a list of variables and function symbols with the help of a stack of partially known terms (i.e. the number of arguments of the main function symbol is less or equal than this symbol's arity). Am I right ?
Looks like if the decoding succeeds, then the preterm it returns could be proven to be a term.
Karl Palmskog (Aug 15 2022 at 15:54):the preterm looks very close to Harrison's original HOL Light FOL term definition:
Datatype:
term = V num | Fn num (term list)
End
I also think a non-dependent preterm definition is going to be the easiest. But you "pay that back" when you have to establish the connection between FOL signatures/languages and terms, which I guess is the conversion from preterm to lists here.
Lessness (Aug 15 2022 at 16:05):Pierre Castéran said:
About decoding: Is the idea you implement as below ?
You decode a list of variables and function symbols with the help of a stack of partially known terms (i.e. the number of arguments of the main function symbol is less or equal than this symbol's arity). Am I right ?
Looks like if the decoding succeeds, then the preterm it returns could be proven to be a term.
Yes, that's the idea.
Pierre Castéran (Aug 15 2022 at 16:10):I've just have a look at Russel's work on Gödel thm. In Ackermann/fol.v, he uses dependent and mutually inductive types.
Record Language : Type :=
language
{Relations : Set; Functions : Set; arity : Relations + Functions -> nat}.
Section First_Order_Logic.
Variable L : Language.
Inductive Term : Set :=
| var : nat -> Term
| apply : forall f : Functions L, Terms (arity L (inr _ f)) -> Term
with Terms : nat -> Set :=
| Tnil : Terms 0
| Tcons : forall n : nat, Term -> Terms n -> Terms (S n).
Scheme Term_Terms_ind := Induction for Term Sort Prop
with Terms_Term_ind := Induction for Terms Sort Prop.
Scheme Term_Terms_rec := Minimality for Term Sort Set
with Terms_Term_rec := Minimality for Terms Sort Set.
Scheme Term_Terms_rec_full := Induction for Term
Sort Set
with Terms_Term_rec_full := Induction for Terms Sort Set.
Inductive Formula : Set :=
| equal : Term -> Term -> Formula
| atomic : forall r : Relations L, Terms (arity L (inl _ r)) -> Formula
| impH : Formula -> Formula -> Formula
| notH : Formula -> Formula
| forallH : nat -> Formula -> Formula.
(* ... *)
I will try luck with my current definition of Term, but it's quite probable I will end with yours. Time will show.
Thank you!
Lessness (Aug 15 2022 at 17:58):I tried to make recursion principle (without using heterogeneous list) by looking at one generated by Scheme for your version of Term.
But it seems weird and not sure how useful it really is. I have problems using it.
Require Import Utf8 List Arith.
Set Implicit Arguments.
Structure Language F R := {
function_arity: F → nat;
relation_arity: R → nat
}.
Inductive preTerm F R V (L: Language F R): Type :=
| variable: V → preTerm V L
| function_term: ∀ (f: F), list (preTerm V L) → preTerm V L.
Arguments variable {_} {_} {_} {L}. (*?*)
Theorem preTerm_recursion F R V (L: Language F R) (P: preTerm V L → Type) (P0: list (preTerm V L) → Type):
(∀ v, P (variable v)) →
(∀ f x, P0 x → P (function_term f x)) →
P0 nil →
(∀ p, P p → ∀ x, P0 x → P0 (p :: x)) →
∀ p, P p.
Proof.
intros H H0 H1 H2. refine (fix IHt (t: preTerm V L) := match t with variable v => H v | function_term f T => _ end).
refine (H0 _ T _). induction T. exact H1. apply H2. apply IHt. auto.
Defined.
Fixpoint term_correct F R V (L: Language F R) (t: preTerm V L): bool :=
match t with
| variable v => true
| function_term f t => andb (Nat.eqb (function_arity L f) (length t)) (forallb (@term_correct F R V L) t)
end.
Definition Term F R V (L: Language F R) := { T: preTerm V L | term_correct T = true }.
Coercion Term_proj1 F R V (L: Language F R) (T: Term V L) := proj1_sig T.
Structure Structure {F R} (L: Language F R) := {
domain: Type;
function: ∀ (f: F) (x: list domain) (H: length x = function_arity L f), domain;
relation: ∀ (r: R) (x: list domain) (H: length x = relation_arity L r), Prop
}.
Definition interpreted_term F R V (L: Language F R) (M: Structure L) (assignment: V → domain M) (T: Term V L): domain M.
Proof.
destruct T as [T H]. revert H. pattern T. induction T using preTerm_recursion with (P0 := _).
+ intros. simpl in *. exact (assignment v).
+ intros. simpl in *. apply andb_prop in H. destruct H.
rewrite forallb_forall in H0. apply beq_nat_true in H.
admit.
Admitted.
Is there some good way to write recursion principle for my version of preTerm, without using that heterogenous list idea?
Paolo Giarrusso (Aug 15 2022 at 19:48):hlist has the right idea: but you can also instantiate P0 to hlist P, or to something else if it makes sense for a specific proof.
Paolo Giarrusso (Aug 15 2022 at 19:49):But honestly, as long as you stick to Coq and not Agda, it might be simpler to keep well-formedness checks in a typing derivation, instead of terms.
Paolo Giarrusso (Aug 15 2022 at 19:50):(even if what Karl wrote is right)
Pierre Castéran (Aug 16 2022 at 07:20):In interpreted_term, I think P0 lshould express (intuitively) : if every term of l respects L, then return a list of values of domain M which has the same length as l.
Defining the interpretation of any well-formed term is indeed a good test for chosing a well-suited representation of terms and formulas.
At present, we met two criteria:
Before chosing one of the four possibilities, it's important to look at all pros and cons of each representation.
Btw, I'm now in charge of maintenance of Russel O'Connor's work on Coq-community. If you have any question about data representations, please don't hesitate.
Lessness (Aug 17 2022 at 20:05):About the proof that decoding function works correctly...
My current state is like this (again approx. 100 lines, because I included anything necessary). I've simplified parts of the decoding function as much as I could and now I'm stuck with the proof (more specifically, with the lemma decode_encode_aux). I don't know how to approach it and any help/suggestion will be appreciated.
Require Import Utf8 List Lia Arith.
Set Implicit Arguments.
Structure Language F R := {
function_arity: F → nat;
relation_arity: R → nat
}.
Inductive preTerm F R V (L: Language F R): Type :=
| variable: V → preTerm V L
| function_term: ∀ (f: F), list (preTerm V L) → preTerm V L.
Arguments variable {_} {_} {_} {L}. (*?*)
Definition preTerm_induction F R V (L: Language F R) (P: preTerm V L → Prop):
(∀ (s: V), P (variable s)) →
(∀ (f: F) (v: list (preTerm V L)), Forall P v → P (function_term f v)) →
∀ T, P T.
Proof.
intros H H0. refine (fix IHt (t: preTerm V L) := match t with variable v => H v | function_term f T => _ end).
refine (H0 _ T _). induction T; constructor; auto.
Defined.
Fixpoint term_correct F R V (L: Language F R) (T: preTerm V L): bool :=
match T with
| variable v => true
| function_term f x => andb (Nat.eqb (length x) (function_arity L f)) (forallb (@term_correct F R V L) x)
end.
Fixpoint encode_preTerm F R V (L: Language F R) (T: preTerm V L): list (F + V) :=
match T with
| variable v => inr v :: nil
| function_term f t => inl f :: flat_map (@encode_preTerm _ _ _ _) t
end.
Definition preterm_free_variables F R V (L: Language F R) (T: preTerm V L): nat :=
match T with
| variable v => 0
| function_term f x => function_arity L f - length x
end.
Fixpoint decode_preTerm_aux F R V (L: Language F R) (l: list (preTerm V L)) (T: preTerm V L): list (preTerm V L) :=
match preterm_free_variables T, l with
| O, function_term f v :: t => decode_preTerm_aux t (function_term f (v ++ T :: nil))
| _, _ => T :: l
end.
Definition decode_preTerm_step F R V (L: Language F R) (t: list (preTerm V L)) (x: F + V): list (preTerm V L) :=
match x with
| inl f => decode_preTerm_aux t (function_term f nil)
| inr v => decode_preTerm_aux t (variable v)
end.
Definition decode_preTerm F R V (L: Language F R) (x: list (F + V)) :=
fold_left (@decode_preTerm_step F R V L) x nil.
Definition term_aux F R V (L: Language F R) (T: preTerm V L): bool :=
match T with
| variable v => true
| function_term f x => andb (Nat.leb (length x) (function_arity L f)) (forallb (@term_correct F R V L) x)
end.
Theorem decode_encode_aux F R V (L: Language F R) (x: preTerm V L) (v: list (preTerm V L))
(Hv: Forall (λ T, term_correct T = true) v)
(Hx: term_correct x = true)
f (H: S (length v) <= function_arity L f):
fold_left (decode_preTerm_step (L:=L)) (encode_preTerm x) (function_term f v :: nil) = function_term f (v ++ x :: nil) :: nil.
Proof.
Admitted.
Theorem decode_encode_thm F R V (L: Language F R) (T: preTerm V L) (H: term_aux T = true):
decode_preTerm L (encode_preTerm T) = T :: nil.
Proof.
induction T using preTerm_induction.
+ compute. auto.
+ simpl in *. apply andb_prop in H. destruct H. apply leb_complete in H. rewrite forallb_forall in H1.
remember (function_arity L f) as W. destruct W.
- unfold decode_preTerm in *. simpl. rewrite <- HeqW. simpl. assert (v = nil).
{ destruct v; auto. simpl in H. lia. }
subst. simpl. reflexivity.
- unfold decode_preTerm in *. simpl in *. rewrite <- HeqW. simpl. induction v using rev_ind.
* simpl. auto.
* simpl in *. rewrite flat_map_app. rewrite fold_left_app. simpl. rewrite app_nil_r.
rewrite IHv. clear IHv.
assert (term_correct x = true). { apply H1. apply in_or_app. simpl. auto. }
assert (term_aux x = true).
{ unfold term_aux, term_correct in *. destruct x; auto. apply andb_prop in H2. destruct H2.
rewrite H3. apply beq_nat_true in H2. rewrite H2. rewrite Nat.leb_refl. auto. }
assert (fold_left (decode_preTerm_step (L:=L)) (encode_preTerm x) nil = x :: nil).
{ apply Forall_app in H0. simpl. destruct H0. apply Forall_inv in H4. apply H4. auto. }
apply decode_encode_aux; auto.
{ rewrite Forall_forall. intros. apply H1. apply in_or_app. auto. }
{ rewrite app_length in H. simpl in H. lia. }
{ apply Forall_app in H0. apply H0. }
{ rewrite app_length in H. simpl in H. lia. }
{ intros. apply H1. apply in_or_app. auto. }
Qed.
Hi,
I'm not an expert in parsing techniques, perhaps it's worth having a look at SF https://softwarefoundations.cis.upenn.edu/lf-current/ImpParser.html
I (successfully) tested your functions with a toy language. Perhaps it's worth documenting the helper functions.
Module Example.
Inductive F : Set := f | g | h.
Definition V := nat.
Inductive R: Set :=.
Definition arity (fn : F) := match fn with f | g => 2 | h => 1 end.
Definition rel_arity (r: R) := 0. (* later *)
Definition L := Build_Language arity rel_arity.
(* f (g x (h (h y))) (h z) *)
Example input : list (F + V) :=
[inl f; inl g; inr 0; inl h; inl h; inr 1; inl h; inr 2 ].
Compute decode_preTerm L input.
Compute decode_preTerm L [inl f; inl g; inr 0].
Compute decode_preTerm L [inl f; inl g; inr 0; inl h].
Compute decode_preTerm L [inl f; inl g; inr 0; inl h; inl h].
Compute decode_preTerm L [inl f; inl g; inr 0; inl h; inl h; inr 1].
Compute decode_preTerm L [inl f; inl g; inr 0; inl h; inl h; inr 1; inl h].
A last remark: during the parsing of alist, the main structure is a list of preterms (which has length 1 at the end).
Did you define a function which computes the preterm associated with such a stack ? It may be used in an invariant which may help you to prove your correctness lemma. Is this stack the v in (Hv: Forall (λ T, term_correct T = true) v) ?
I'm not sure, but in the test below, the stack looks to contain partially filled terms, which may not satisfy term_correct.
Compute decode_preTerm L [inl f; inl g; inr 0; inl h; inl h].
(*
= [function_term h []; function_term h []; function_term g [variable 0]; function_term f []]
: list (preTerm nat L)
*)
Thank you very much! Apologies for not replying long time, was busy. (From edit history of your post I can see that I was away for many hours.)
Yes, I had tests using toy language. Will think about useful invariant as it seems to be the right way.
Lessness (Aug 20 2022 at 17:56):Okay, for now I have given up (with my version of encode/decode) functions for (pre)Terms. In the future I will need to write the same thing for (pre)Formulas and it should be even harder.
So... I'm decided to take GenTree encode and decode functions from https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/choice.v. But I got stuck with the proof of the lemma CodeK which is written using SSReflect tactics. (They are like foreign language for me for now. :sweat_smile:)
Lemma codeK : pcancel encode decode.
Proof.
move=> t; rewrite /decode; set fs := (_, _).
suffices ->: foldr decode_step fs (encode t) = (t :: fs.1, fs.2) by [].
elim: t => //= n f IHt in (fs) *; elim: f IHt => //= t f IHf [].
by rewrite rcons_cat foldr_cat => -> /= /IHf[-> -> ->].
Qed.
Maybe someone can translate them into standard Coq tactics or maybe explain what's going on here... If so, thanks in advance.
I got this far for now.
Theorem encode_decode_tree_thm T (x: tree T): decode_tree (encode_tree x) = Some x.
Proof.
unfold decode_tree. set (fs := (nil, nil)).
cut (fold_right (@decode_tree_step _) fs (encode_tree x) = (x :: fst fs, snd fs)).
intros. rewrite H. simpl. auto.
{ admit. }
Admitted.
I managed to prove the lemma. Yay! :)
Lessness (Aug 26 2022 at 10:43):Hello again!
I have proved countability of preTerms and preFormulas (assuming countability of F, R, V parameters). Now I want to prove the countability of Terms and Formulas. Should I go into "setoid hell"? Or are there some option to stay away from it.
(Terms are preTerms, for example, T with term_correct T = true.)
Paolo Giarrusso (Aug 26 2022 at 13:59):You needn't squash type term_correct T = true to a singleton via setoids, if that's what you're thinking of: that's already is a singleton (because of decidable equality on booleans and Hedberg's theorem)
Gaëtan Gilbert (Aug 26 2022 at 17:20):I think it should be possible to prove forall A (P : A -> bool), countable A -> not (finite {x | P x = true}) -> countable {x | P x = true}
then you just need to provide a "not finite" proof for terms
Lessness (Aug 26 2022 at 20:29):Paolo Giarrusso said:
You needn't squash type
term_correct T = trueto a singleton via setoids, if that's what you're thinking of: that's already is a singleton (because of decidable equality on booleans and Hedberg's theorem)
So, I should be able to prove the theorem Theorem aux A (P: A → bool): ∀ x (p1 p2: P x = true), p1 = p2., right?
Enrico Tassi (Aug 26 2022 at 20:36):Yes, but the proof is not easy ;-)
Here one: https://github.com/math-comp/math-comp/blob/c66a532bc7878c366acfe5203083fb3dcbb31d3e/mathcomp/ssreflect/eqtype.v#L307-L314
Enrico Tassi (Aug 26 2022 at 20:37):It is not just for bool, but for any type with decidable equality (hence bool).
Enrico Tassi (Aug 26 2022 at 20:38):the proof is hard because dependent elimination is tricky, you need to set things up so that the elimination does not break typing of the goal.
Enrico Tassi (Aug 26 2022 at 20:38):You can find the same proof also in the stdlib of Coq, but I'm too lazy to find it for you.
Enrico Tassi (Aug 26 2022 at 20:39):(it is really the same proof)
Gaëtan Gilbert (Aug 26 2022 at 20:40):Eqdep_dec.eq_proofs_unicity
Lessness (Aug 26 2022 at 21:08):Thank you very much!
Lessness (Aug 26 2022 at 21:10):Now I have proved the countability of Terms and Formulas. :tada:
Notification Bot (Aug 26 2022 at 21:10):Lessness has marked this topic as resolved.
Last updated: Oct 04 2023 at 22:01 UTC