Merge branch 'ralf/tele' into 'master'

fix λ.. printing and test it

See merge request !51

Makefile.coq.local

@@ -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 $@

tests/telescopes.ref

+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

tests/telescopes.v

+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.

theories/telescopes.v

@@ -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,9 +141,9 @@ 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").
+   format "'[  ' 'λ..'  x  ..  y ']' ,  e") : stdpp_scope.
 
 (** Telescopic quantifiers *)
 Definition tforall {TT : tele} (Ψ : TT → Prop) : Prop :=