Fil-C on Nix

Filnix wiki

the formal campaign

rocq/theories/Term.v

Ground Prolog terms, the shape every nanofil product has before it means anything: an integer, an atom, a compound of a name and arguments, or a proper list.

The model uses them twice. The names of nanofil's intermediate representation (IR), its temporaries, block labels, symbols and named locals, are ground terms, compared only for equality, as ir.pl says: "Temps are ground names". And a module or an outcome crosses between Prolog and the extracted model as a term, which Transport.v decodes into the syntax of Syntax.v and encodes back.

From Stdlib Require Import String ZArith List Bool Ascii
Import ListNotations

A ground Prolog term, one constructor per form. A proper list is its own form rather than nested '[|]'/2 compounds, so that decoding a list of blocks or instructions is a map.

19Inductive term: Type ≔
|TInt
n : Z
the integer n
|TAtom
a : string
the atom a, [ ] included
|TApp
f : string args : listterm
the compound f(A1, ..., An), with at least one argument
|TList
ts : listterm
the proper list [T1, ..., Tn]

Term equality, structural, as Prolog's ==/2 on ground terms.

26Fixpoint term_eqbt u : term : bool ≔
let fix list_eqb ts us : listterm : bool ≔
match ts, us with
[ ], [ ]
⇒
true
t :: ts′, u :: us′
⇒
term_eqbt u && list_eqbts′ us′
_, _
⇒
false
in
match t, u with
TIntn, TIntm
⇒
Z.eqbn m
TAtoma, TAtomb
⇒
String.eqba b
TAppf ts, TAppg us
⇒
String.eqbf g && list_eqbts us
TListts, TListus
⇒
list_eqbts us
_, _
⇒
false

term_eqb is sound: two terms t and u it calls equal are the same term, so a name found by comparing is the very name asked for.

43Lemma term_eqb_eq
∀ t u
term_eqbt u = true
t = u
Explore proof 22 tactics

Initial goal

⊢
∀t u : term, term_eqbt u = true → t = u

fix IH 1

IH :
∀t u : term, term_eqbt u = true → t = u
⊢
∀t u : term, term_eqbt u = true → t = u

intros t u H

IH :
∀t u : term, term_eqbt u = true → t = u
t, u :
term
H :
term_eqbt u = true
⊢
t = u

destruct t as n | a | f ts | ts , u as n′ | a′ | f′ us | us ; simpl in H ; try discriminate H

4 open

IH :
∀t u : term, term_eqbt u = true → t = u
n, n′ :
Z
H :
n =? n′%Z = true
⊢
TIntn = TIntn′
focused goal
IH :
∀t u : term, term_eqbt u = true → t = u
a, a′ :
string
H :
a =? a′%string = true
⊢
TAtoma = TAtoma′
focused goal
IH :
∀t u : term, term_eqbt u = true → t = u
f :
string
ts :
listterm
f′ :
string
us :
listterm
H :
f =? f′%string
&&
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
⊢
TAppf ts = TAppf′ us
focused goal
IH :
∀t u : term, term_eqbt u = true → t = u
ts, us :
listterm
H :
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
⊢
TListts = TListus

–f_equal

4 open

IH :
∀t u : term, term_eqbt u = true → t = u
n, n′ :
Z
H :
n =? n′%Z = true
⊢
n = n′
deferred goal
IH :
∀t u : term, term_eqbt u = true → t = u
a, a′ :
string
H :
a =? a′%string = true
⊢
TAtoma = TAtoma′
deferred goal
IH :
∀t u : term, term_eqbt u = true → t = u
f :
string
ts :
listterm
f′ :
string
us :
listterm
H :
f =? f′%string
&&
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
⊢
TAppf ts = TAppf′ us
deferred goal
IH :
∀t u : term, term_eqbt u = true → t = u
ts, us :
listterm
H :
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
⊢
TListts = TListus

apply Z.eqb_eq

4 open

IH :
∀t u : term, term_eqbt u = true → t = u
n, n′ :
Z
H :
n =? n′%Z = true
⊢
n =? n′%Z = true
deferred goal
IH :
∀t u : term, term_eqbt u = true → t = u
a, a′ :
string
H :
a =? a′%string = true
⊢
TAtoma = TAtoma′
deferred goal
IH :
∀t u : term, term_eqbt u = true → t = u
f :
string
ts :
listterm
f′ :
string
us :
listterm
H :
f =? f′%string
&&
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
⊢
TAppf ts = TAppf′ us
deferred goal
IH :
∀t u : term, term_eqbt u = true → t = u
ts, us :
listterm
H :
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
⊢
TListts = TListus

exact H

3 open

deferred goal
IH :
∀t u : term, term_eqbt u = true → t = u
a, a′ :
string
H :
a =? a′%string = true
⊢
TAtoma = TAtoma′
deferred goal
IH :
∀t u : term, term_eqbt u = true → t = u
f :
string
ts :
listterm
f′ :
string
us :
listterm
H :
f =? f′%string
&&
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
⊢
TAppf ts = TAppf′ us
deferred goal
IH :
∀t u : term, term_eqbt u = true → t = u
ts, us :
listterm
H :
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
⊢
TListts = TListus

–f_equal

3 open

IH :
∀t u : term, term_eqbt u = true → t = u
a, a′ :
string
H :
a =? a′%string = true
⊢
a = a′
deferred goal
IH :
∀t u : term, term_eqbt u = true → t = u
f :
string
ts :
listterm
f′ :
string
us :
listterm
H :
f =? f′%string
&&
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
⊢
TAppf ts = TAppf′ us
deferred goal
IH :
∀t u : term, term_eqbt u = true → t = u
ts, us :
listterm
H :
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
⊢
TListts = TListus

apply String.eqb_eq

3 open

IH :
∀t u : term, term_eqbt u = true → t = u
a, a′ :
string
H :
a =? a′%string = true
⊢
a =? a′%string = true
deferred goal
IH :
∀t u : term, term_eqbt u = true → t = u
f :
string
ts :
listterm
f′ :
string
us :
listterm
H :
f =? f′%string
&&
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
⊢
TAppf ts = TAppf′ us
deferred goal
IH :
∀t u : term, term_eqbt u = true → t = u
ts, us :
listterm
H :
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
⊢
TListts = TListus

exact H

2 open

deferred goal
IH :
∀t u : term, term_eqbt u = true → t = u
f :
string
ts :
listterm
f′ :
string
us :
listterm
H :
f =? f′%string
&&
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
⊢
TAppf ts = TAppf′ us
deferred goal
IH :
∀t u : term, term_eqbt u = true → t = u
ts, us :
listterm
H :
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
⊢
TListts = TListus

–apply andb_true_iff in H as Hf Hl

2 open

IH :
∀t u : term, term_eqbt u = true → t = u
f :
string
ts :
listterm
f′ :
string
us :
listterm
Hf :
f =? f′%string = true
Hl :
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
⊢
TAppf ts = TAppf′ us
deferred goal
IH :
∀t u : term, term_eqbt u = true → t = u
ts, us :
listterm
H :
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
⊢
TListts = TListus

apply String.eqb_eq in Hf

2 open

IH :
∀t u : term, term_eqbt u = true → t = u
f :
string
ts :
listterm
f′ :
string
us :
listterm
Hf :
f = f′
Hl :
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
⊢
TAppf ts = TAppf′ us
deferred goal
IH :
∀t u : term, term_eqbt u = true → t = u
ts, us :
listterm
H :
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
⊢
TListts = TListus

subst f′

2 open

IH :
∀t u : term, term_eqbt u = true → t = u
f :
string
ts, us :
listterm
Hl :
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
⊢
TAppf ts = TAppf us
deferred goal
IH :
∀t u : term, term_eqbt u = true → t = u
ts, us :
listterm
H :
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
⊢
TListts = TListus

f_equal

2 open

IH :
∀t u : term, term_eqbt u = true → t = u
f :
string
ts, us :
listterm
Hl :
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
⊢
ts = us
deferred goal
IH :
∀t u : term, term_eqbt u = true → t = u
ts, us :
listterm
H :
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
⊢
TListts = TListus

revert us Hl

2 open

IH :
∀t u : term, term_eqbt u = true → t = u
f :
string
ts :
listterm
⊢
∀ us : listterm  ,
fix list_eqb ts0 us0 : listterm {struct ts0} : bool ≔
match ts0 with
[ ]
⇒
match us0 with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us0 with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
→
ts = us
deferred goal
IH :
∀t u : term, term_eqbt u = true → t = u
ts, us :
listterm
H :
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
⊢
TListts = TListus

induction ts as | t ts IHl ; intros | u us Hl ; simpl in Hl ; try discriminate Hl ; auto

2 open

IH :
∀t u : term, term_eqbt u = true → t = u
f :
string
t :
term
ts :
listterm
IHl :
∀ us : listterm  ,
fix list_eqb ts us0 : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us0 with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us0 with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
→
ts = us
u :
term
us :
listterm
Hl :
term_eqbt u
&&
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
⊢
t :: ts = u :: us
deferred goal
IH :
∀t u : term, term_eqbt u = true → t = u
ts, us :
listterm
H :
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
⊢
TListts = TListus

apply andb_true_iff in Hl as H1 H2

2 open

IH :
∀t u : term, term_eqbt u = true → t = u
f :
string
t :
term
ts :
listterm
IHl :
∀ us : listterm  ,
fix list_eqb ts us0 : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us0 with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us0 with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
→
ts = us
u :
term
us :
listterm
H1 :
term_eqbt u = true
H2 :
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
⊢
t :: ts = u :: us
deferred goal
IH :
∀t u : term, term_eqbt u = true → t = u
ts, us :
listterm
H :
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
⊢
TListts = TListus

f_equal ; apply IH ; exact H1 | apply IHl ; exact H2

deferred goal
IH :
∀t u : term, term_eqbt u = true → t = u
ts, us :
listterm
H :
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
⊢
TListts = TListus

–f_equal

IH :
∀t u : term, term_eqbt u = true → t = u
ts, us :
listterm
H :
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
⊢
ts = us

revert us H

IH :
∀t u : term, term_eqbt u = true → t = u
ts :
listterm
⊢
∀ us : listterm  ,
fix list_eqb ts0 us0 : listterm {struct ts0} : bool ≔
match ts0 with
[ ]
⇒
match us0 with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us0 with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
→
ts = us

induction ts as | t ts IHl ; intros | u us Hl ; simpl in Hl ; try discriminate Hl ; auto

IH :
∀t u : term, term_eqbt u = true → t = u
t :
term
ts :
listterm
IHl :
∀ us : listterm  ,
fix list_eqb ts us0 : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us0 with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us0 with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
→
ts = us
u :
term
us :
listterm
Hl :
term_eqbt u
&&
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
⊢
t :: ts = u :: us

apply andb_true_iff in Hl as H1 H2

IH :
∀t u : term, term_eqbt u = true → t = u
t :
term
ts :
listterm
IHl :
∀ us : listterm  ,
fix list_eqb ts us0 : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us0 with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us0 with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
→
ts = us
u :
term
us :
listterm
H1 :
term_eqbt u = true
H2 :
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts us
=
true
⊢
t :: ts = u :: us

f_equal ; apply IH ; exact H1 | apply IHl ; exact H2

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
fix IH 1
intros t u H
destruct t as n | a | f ts | ts , u as n′ | a′ | f′ us | us ; simpl in H ; try discriminate H
–f_equal
apply Z.eqb_eq
exact H
–f_equal
apply String.eqb_eq
exact H
–apply andb_true_iff in H as Hf Hl
apply String.eqb_eq in Hf
subst f′
f_equal
revert us Hl
induction ts as | t ts IHl ; intros | u us Hl ; simpl in Hl ; try discriminate Hl ; auto
apply andb_true_iff in Hl as H1 H2
f_equal ; apply IH ; exact H1 | apply IHl ; exact H2
–f_equal
revert us H
induction ts as | t ts IHl ; intros | u us Hl ; simpl in Hl ; try discriminate Hl ; auto
apply andb_true_iff in Hl as H1 H2
f_equal ; apply IH ; exact H1 | apply IHl ; exact H2

Every term t is term_eqb-equal to itself, as Prolog's ==/2 holds of a term and itself.

59Lemma term_eqb_refl
∀ t
term_eqbt t = true
Explore proof 13 tactics

Initial goal

⊢
∀t : term, term_eqbt t = true

fix IH 1

IH :
∀t : term, term_eqbt t = true
⊢
∀t : term, term_eqbt t = true

intros t

IH :
∀t : term, term_eqbt t = true
t :
term
⊢
term_eqbt t = true

destruct t as n | a | f ts | ts ; simpl

4 open

IH :
∀t : term, term_eqbt t = true
n :
Z
⊢
n =? n%Z = true
focused goal
IH :
∀t : term, term_eqbt t = true
a :
string
⊢
a =? a%string = true
focused goal
IH :
∀t : term, term_eqbt t = true
f :
string
ts :
listterm
⊢
f =? f%string
&&
fix list_eqb ts0 us : listterm {struct ts0} : bool ≔
match ts0 with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts ts
=
true
focused goal
IH :
∀t : term, term_eqbt t = true
ts :
listterm
⊢
fix list_eqb ts0 us : listterm {struct ts0} : bool ≔
match ts0 with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts ts
=
true

–apply Z.eqb_refl

3 open

deferred goal
IH :
∀t : term, term_eqbt t = true
a :
string
⊢
a =? a%string = true
deferred goal
IH :
∀t : term, term_eqbt t = true
f :
string
ts :
listterm
⊢
f =? f%string
&&
fix list_eqb ts0 us : listterm {struct ts0} : bool ≔
match ts0 with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts ts
=
true
deferred goal
IH :
∀t : term, term_eqbt t = true
ts :
listterm
⊢
fix list_eqb ts0 us : listterm {struct ts0} : bool ≔
match ts0 with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts ts
=
true

–apply String.eqb_refl

2 open

deferred goal
IH :
∀t : term, term_eqbt t = true
f :
string
ts :
listterm
⊢
f =? f%string
&&
fix list_eqb ts0 us : listterm {struct ts0} : bool ≔
match ts0 with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts ts
=
true
deferred goal
IH :
∀t : term, term_eqbt t = true
ts :
listterm
⊢
fix list_eqb ts0 us : listterm {struct ts0} : bool ≔
match ts0 with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts ts
=
true

–rewrite String.eqb_refl

2 open

IH :
∀t : term, term_eqbt t = true
f :
string
ts :
listterm
⊢
true
&&
fix list_eqb ts0 us : listterm {struct ts0} : bool ≔
match ts0 with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts ts
=
true
deferred goal
IH :
∀t : term, term_eqbt t = true
ts :
listterm
⊢
fix list_eqb ts0 us : listterm {struct ts0} : bool ≔
match ts0 with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts ts
=
true

simpl

2 open

IH :
∀t : term, term_eqbt t = true
f :
string
ts :
listterm
⊢
fix list_eqb ts0 us : listterm {struct ts0} : bool ≔
match ts0 with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts ts
=
true
deferred goal
IH :
∀t : term, term_eqbt t = true
ts :
listterm
⊢
fix list_eqb ts0 us : listterm {struct ts0} : bool ≔
match ts0 with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts ts
=
true

induction ts as | t ts IHl ; simpl ; auto

2 open

IH :
∀t : term, term_eqbt t = true
f :
string
t :
term
ts :
listterm
IHl :
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts ts
=
true
⊢
term_eqbt t
&&
fix list_eqb ts0 us : listterm {struct ts0} : bool ≔
match ts0 with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t0 :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt0 u && list_eqbts′ us′
ts ts
=
true
deferred goal
IH :
∀t : term, term_eqbt t = true
ts :
listterm
⊢
fix list_eqb ts0 us : listterm {struct ts0} : bool ≔
match ts0 with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts ts
=
true

rewrite IH

2 open

IH :
∀t : term, term_eqbt t = true
f :
string
t :
term
ts :
listterm
IHl :
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts ts
=
true
⊢
true
&&
fix list_eqb ts0 us : listterm {struct ts0} : bool ≔
match ts0 with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t0 :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt0 u && list_eqbts′ us′
ts ts
=
true
deferred goal
IH :
∀t : term, term_eqbt t = true
ts :
listterm
⊢
fix list_eqb ts0 us : listterm {struct ts0} : bool ≔
match ts0 with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts ts
=
true

exact IHl

deferred goal
IH :
∀t : term, term_eqbt t = true
ts :
listterm
⊢
fix list_eqb ts0 us : listterm {struct ts0} : bool ≔
match ts0 with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts ts
=
true

–induction ts as | t ts IHl ; simpl ; auto

IH :
∀t : term, term_eqbt t = true
t :
term
ts :
listterm
IHl :
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts ts
=
true
⊢
term_eqbt t
&&
fix list_eqb ts0 us : listterm {struct ts0} : bool ≔
match ts0 with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t0 :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt0 u && list_eqbts′ us′
ts ts
=
true

rewrite IH

IH :
∀t : term, term_eqbt t = true
t :
term
ts :
listterm
IHl :
fix list_eqb ts us : listterm {struct ts} : bool ≔
match ts with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt u && list_eqbts′ us′
ts ts
=
true
⊢
true
&&
fix list_eqb ts0 us : listterm {struct ts0} : bool ≔
match ts0 with
[ ]
⇒
match us with
[ ]
⇒
true
_ :: _
⇒
false
t0 :: ts′
⇒
match us with
[ ]
⇒
false
u :: us′
⇒
term_eqbt0 u && list_eqbts′ us′
ts ts
=
true

exact IHl

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
fix IH 1
intros t
destruct t as n | a | f ts | ts ; simpl
–apply Z.eqb_refl
–apply String.eqb_refl
–rewrite String.eqb_refl
simpl
induction ts as | t ts IHl ; simpl ; auto
rewrite IH
exact IHl
–induction ts as | t ts IHl ; simpl ; auto
rewrite IH
exact IHl

A name of the IR: a temporary, a block label, a symbol or a named local, any ground term.

71Definition name ≔
term

Equality of names, which is term_eqb.

74Definition name_eqb: name → name → bool ≔
term_eqb

As memberchk(Key-V, Pairs): the value of the first pair of the association list ps whose key is k, if any. Prolog's library(assoc) and the association lists here agree on every lookup: a key is put once, or replaced.

80Fixpoint lookupA : Type k : name ps : listname × A : optionA ≔
match ps with
[ ]
⇒
None
k′, v :: ps′
⇒
name_eqbk k′
→
Somev
else
lookupk ps′

As put_assoc(Key, Assoc0, V, Assoc): the association list ps with k now mapped to v, in front, and k's old pair dropped.

88Definition putA : Type k : name v : A ps : listname × A : listname × A ≔
k, v :: filterλp ⇒ negbname_eqbk fstp ps
Open Scope Z_scope

The code of t, a one-character atom, as char_code/2 gives it, for the codes 0 to 2047: one byte below 128, or a two-byte UTF-8 sequence. Any other term, or an atom of another code, has none.

97Definition char_codet : term : optionZ ≔
match t with
TAtomStringc EmptyString
⇒
let a ≔ Z.of_natnat_of_asciic in
a <? 128
→
Somea
else
None
TAtomStringc1 Stringc2 EmptyString
⇒
let a ≔ Z.of_natnat_of_asciic1 in
let b ≔ Z.of_natnat_of_asciic2 in
192 ≤? a && a <? 224 && 128 ≤? b && b <? 192
→
Somea − 192 × 64 + b − 128
else
None
_
⇒
None