Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
PierreMarie Pédrot
Iris
Commits
91d50c60
Commit
91d50c60
authored
Jun 21, 2016
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
More hlist stuff.
parent
c885513d
Changes
3
Hide whitespace changes
Inline
Sidebyside
Showing
3 changed files
with
41 additions
and
11 deletions
+41
11
algebra/upred_hlist.v
algebra/upred_hlist.v
+2
2
prelude/hlist.v
prelude/hlist.v
+38
7
proofmode/tactics.v
proofmode/tactics.v
+1
2
No files found.
algebra/upred_hlist.v
View file @
91d50c60
...
...
@@ 25,7 +25,7 @@ Proof.
+
apply
exist_elim
=>
x
;
rewrite
IH
;
apply
exist_elim
=>
xs
.
by
rewrite
(
exist_intro
(
hcons
x
xs
)).

apply
exist_elim
=>
xs
;
induction
xs
as
[
A
As
x
xs
IH
]
;
simpl
;
auto
.
by
rewrite
(
exist_intro
x
).
by
rewrite
(
exist_intro
x
)
IH
.
Qed
.
Lemma
hforall_forall
{
As
B
}
(
f
:
himpl
As
B
)
(
Φ
:
B
→
uPred
M
)
:
...
...
@@ 33,7 +33,7 @@ Lemma hforall_forall {As B} (f : himpl As B) (Φ : B → uPred M) :
Proof
.
apply
(
anti_symm
_
).

apply
forall_intro
=>
xs
;
induction
xs
as
[
A
As
x
xs
IH
]
;
simpl
;
auto
.
by
rewrite
(
forall_elim
x
).
by
rewrite
(
forall_elim
x
)
IH
.

induction
As
as
[
A
As
IH
]
;
simpl
.
+
by
rewrite
(
forall_elim
hnil
)
.
+
apply
forall_intro
=>
x
;
rewrite

IH
;
apply
forall_intro
=>
xs
.
...
...
prelude/hlist.v
View file @
91d50c60
From
iris
.
prelude
Require
Import
base
.
From
iris
.
prelude
Require
Import
tactics
.
(* Not using [list Type] in order to avoid universe inconsistencies *)
Inductive
tlist
:
=
tnil
:
tlist

tcons
:
Type
→
tlist
→
tlist
.
...
...
@@ 7,22 +7,53 @@ Inductive hlist : tlist → Type :=

hnil
:
hlist
tnil

hcons
{
A
As
}
:
A
→
hlist
As
→
hlist
(
tcons
A
As
).
Fixpoint
tapp
(
As
Bs
:
tlist
)
:
tlist
:
=
match
As
with
tnil
=>
Bs

tcons
A
As
=>
tcons
A
(
tapp
As
Bs
)
end
.
Fixpoint
happ
{
As
Bs
}
(
xs
:
hlist
As
)
(
ys
:
hlist
Bs
)
:
hlist
(
tapp
As
Bs
)
:
=
match
xs
with
hnil
=>
ys

hcons
_
_
x
xs
=>
hcons
x
(
happ
xs
ys
)
end
.
Fixpoint
hhead
{
A
As
}
(
xs
:
hlist
(
tcons
A
As
))
:
A
:
=
match
xs
with
hnil
=>
()

hcons
_
_
x
_
=>
x
end
.
Fixpoint
htail
{
A
As
}
(
xs
:
hlist
(
tcons
A
As
))
:
hlist
As
:
=
match
xs
with
hnil
=>
()

hcons
_
_
_
xs
=>
xs
end
.
Fixpoint
hheads
{
As
Bs
}
:
hlist
(
tapp
As
Bs
)
→
hlist
As
:
=
match
As
with

tnil
=>
λ
_
,
hnil

tcons
A
As
=>
λ
xs
,
hcons
(
hhead
xs
)
(
hheads
(
htail
xs
))
end
.
Fixpoint
htails
{
As
Bs
}
:
hlist
(
tapp
As
Bs
)
→
hlist
Bs
:
=
match
As
with

tnil
=>
id

tcons
A
As
=>
λ
xs
,
htails
(
htail
xs
)
end
.
Fixpoint
himpl
(
As
:
tlist
)
(
B
:
Type
)
:
Type
:
=
match
As
with
tnil
=>
B

tcons
A
As
=>
A
→
himpl
As
B
end
.
Definition
happly
{
As
B
}
(
f
:
himpl
As
B
)
(
xs
:
hlist
As
)
:
B
:
=
Definition
hinit
{
B
}
(
y
:
B
)
:
himpl
tnil
B
:
=
y
.
Definition
hlam
{
A
As
B
}
(
f
:
A
→
himpl
As
B
)
:
himpl
(
tcons
A
As
)
B
:
=
f
.
Arguments
hlam
_
_
_
_
_
/.
Definition
hcurry
{
As
B
}
(
f
:
himpl
As
B
)
(
xs
:
hlist
As
)
:
B
:
=
(
fix
go
As
xs
:
=
match
xs
in
hlist
As
return
himpl
As
B
→
B
with

hnil
=>
λ
f
,
f

hcons
A
As
x
xs
=>
λ
f
,
go
As
xs
(
f
x
)
end
)
_
xs
f
.
Coercion
happly
:
himpl
>>
Funclass
.
Coercion
hcurry
:
himpl
>>
Funclass
.
Fixpoint
huncurry
{
As
B
}
:
(
hlist
As
→
B
)
→
himpl
As
B
:
=
match
As
with

tnil
=>
λ
f
,
f
hnil

tcons
x
xs
=>
λ
f
,
hlam
(
λ
x
,
huncurry
(
f
∘
hcons
x
))
end
.
Lemma
hcurry_uncurry
{
As
B
}
(
f
:
hlist
As
→
B
)
xs
:
huncurry
f
xs
=
f
xs
.
Proof
.
by
induction
xs
as
[
A
As
x
xs
IH
]
;
simpl
;
rewrite
?IH
.
Qed
.
Fixpoint
hcompose
{
As
B
C
}
(
f
:
B
→
C
)
{
struct
As
}
:
himpl
As
B
→
himpl
As
C
:
=
match
As
with

tnil
=>
f

tcons
A
As
=>
λ
g
x
,
hcompose
f
(
g
x
)

tcons
A
As
=>
λ
g
,
hlam
(
λ
x
,
hcompose
f
(
g
x
)
)
end
.
Definition
hinit
{
B
}
(
y
:
B
)
:
himpl
tnil
B
:
=
y
.
Definition
hlam
{
A
As
B
}
(
f
:
A
→
himpl
As
B
)
:
himpl
(
tcons
A
As
)
B
:
=
f
.
proofmode/tactics.v
View file @
91d50c60
...
...
@@ 11,7 +11,6 @@ Declare Reduction env_cbv := cbv [
bool_eq_dec
bool_rec
bool_rect
bool_dec
eqb
andb
(* bool *)
assci_eq_dec
ascii_to_digits
Ascii
.
ascii_dec
Ascii
.
ascii_rec
Ascii
.
ascii_rect
string_eq_dec
string_rec
string_rect
(* strings *)
himpl
happly
env_persistent
env_spatial
envs_persistent
envs_lookup
envs_lookup_delete
envs_delete
envs_app
envs_simple_replace
envs_replace
envs_split
envs_clear_spatial
].
...
...
@@ 135,7 +134,7 @@ Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
eapply
tac_forall_specialize
with
_
H
_
_
_
xs
;
(* (i:=H) (a:=x) *)
[
env_cbv
;
reflexivity

fail
1
"iSpecialize:"
H
"not found"

apply
_

fail
1
"iSpecialize:"
H
"not a forall of the right arity or type"

env_cbv
;
reflexivity
]

cbn
[
himpl
hcurry
]
;
reflexivity
]
end
.
Local
Tactic
Notation
"iSpecializePat"
constr
(
H
)
constr
(
pat
)
:
=
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment