Commit 05ffdc9b authored by Ralf Jung's avatar Ralf Jung

fix λ.. printing and test it

parent 53189fab
......@@ -8,7 +8,8 @@ test: $(TESTFILES:.v=.vo)
.PHONY: test
COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
COQ_BROKEN=
COQ_OLD=$(shell echo "$(COQ_VERSION)" | egrep "^8\.7\b" > /dev/null && echo 1)
COQ_MINOR_VERSION=$(shell echo "$(COQ_VERSION)" | egrep '^[0-9]+\.[0-9]+\b' -o)
# Can't use pipes because that discards error codes and dash provides no way to control that.
# Also egrep errors if it doesn't match anything, we have to ignore that.
......@@ -21,17 +22,19 @@ tests/.coqdeps.d: $(TESTFILES)
-include tests/.coqdeps.d
$(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref)
$(SHOW)$(if $(MAKE_REF),COQTEST [ref],$(if $(COQ_BROKEN),COQTEST [ignored],COQTEST)) $<
$(HIDE)TEST="$$(basename -s .v $<)" && \
if test -f "tests/$$TEST.$(COQ_MINOR_VERSION).ref"; then \
REF="tests/$$TEST.$(COQ_MINOR_VERSION).ref"; \
else \
REF="tests/$$TEST.ref"; \
fi && \
echo $(if $(MAKE_REF),"COQTEST [ref] `basename "$$REF"`","COQTEST$(if $(COQ_OLD), [ignored],) `basename "$$REF"`") && \
TMPFILE="$$(mktemp)" && \
$(TIMER) $(COQ_TEST) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< > "$$TMPFILE" && \
($(REF_FILTER) < "$$TMPFILE" > "$$TMPFILE.filtered" || true) && \
$(if $(MAKE_REF), \
mv "$$TMPFILE.filtered" "tests/$$TEST.ref", \
$(if $(COQ_BROKEN), \
true, \
diff -u "tests/$$TEST.ref" "$$TMPFILE.filtered" \
) \
mv "$$TMPFILE.filtered" "$$REF", \
$(if $(COQ_OLD),true,diff -u "$$REF" "$$TMPFILE.filtered") \
) && \
rm -f "$$TMPFILE" "$$TMPFILE.filtered" && \
touch $@
1 subgoal
X : tele
α, β, γ1, γ2 : X → Prop
============================
accessor α β γ1 → accessor α β (λ.. x : X, γ1 x ∨ γ2 x)
1 subgoal
X : tele
α, β, γ1, γ2 : X → Prop
============================
∀.. x : X, γ1 x → (λ.. x0 : X, γ1 x0 ∨ γ2 x0) x
1 subgoal
X : tele
α, β, γ1, γ2 : X → Prop
x : X
Hγ : γ1 x
============================
γ1 x ∨ γ2 x
From stdpp Require Import tactics telescopes.
Section accessor.
(* This is like Iris' accessors, but in Prop. Just to play with telescopes. *)
Definition accessor {X : tele} (α β γ : X Prop) : Prop :=
.. x, α x (β x γ x).
(* Working with abstract telescopes. *)
Section tests.
Context {X : tele}.
Implicit Types α β γ : X Prop.
Lemma acc_mono α β γ1 γ2 :
(.. x, γ1 x γ2 x)
accessor α β γ1 accessor α β γ2.
Proof.
unfold accessor. rewrite tforall_forall, !texist_exist.
intros Hγ12 Hacc. destruct Hacc as [x' [Hα Hclose]]. exists x'.
split; [done|]. intros Hβ. apply Hγ12, Hclose. done.
Qed.
Lemma acc_mono_disj α β γ1 γ2 :
accessor α β γ1 accessor α β (λ.. x, γ1 x γ2 x).
Proof.
Show.
apply acc_mono. Show.
rewrite tforall_forall. intros x Hγ. rewrite tele_app_bind. Show.
left. done.
Qed.
End tests.
......@@ -48,7 +48,8 @@ Definition tele_app {TT : tele} {T} (f : TT -t> T) : tele_arg TT → T :=
Arguments tele_app {!_ _} _ !_ /.
Coercion tele_arg : tele >-> Sortclass.
Coercion tele_app : tele_fun >-> Funclass.
(* This is a local coercion because otherwise, the "λ.." notation stops working. *)
Local Coercion tele_app : tele_fun >-> Funclass.
(** Inversion lemma for [tele_arg] *)
Lemma tele_arg_inv {TT : tele} (a : TT) :
......@@ -140,7 +141,7 @@ Notation "'[tele_arg' ]" := (TargO)
binder so that, after simplifying, this matches the way we typically write
notations involving telescopes. *)
Notation "'λ..' x .. y , e" :=
(tele_app $ tele_bind (λ x, .. (tele_app $ tele_bind (λ y, e)) .. ))
(tele_app (tele_bind (λ x, .. (tele_app (tele_bind (λ y, e))) .. )))
(at level 200, x binder, y binder, right associativity,
format "'[ ' 'λ..' x .. y ']' , e").
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment