| \documentclass{article} | |
| \usepackage{lmodern} | |
| \usepackage[T1]{fontenc} | |
| \title{Hi} | |
| \begin{document} | |
| \maketitle | |
| \end{document} |
| (** Support writing external hints for lemmas that must not be applied twice for a goal. *) | |
| (* The usedLemma and un_usedLemma marker is taken from Crush.v (where they were called done and un_done). *) | |
| (** Devious marker predicate to use for encoding state within proof goals *) | |
| Definition usedLemma {T : Type} (x : T) := True. | |
| (** After a round of application with the above, we will have a lot of junk [usedLemma] markers to clean up; hence this tactic. *) | |
| Ltac un_usedLemma := | |
| repeat match goal with | |
| | [ H : usedLemma _ |- _ ] => clear H |
| From iris.proofmode Require Import tactics. | |
| From iris.bi Require Import bi. | |
| Import bi. | |
| Section sbi_instances. | |
| Context {PROP : sbi}. | |
| Implicit Types P Q R : PROP. | |
| Global Instance elim_modal_fupd_fupd_mask_frame_empty `{BiFUpd PROP} p E1 E1' E3 P Q : | |
| ElimModal (E1 ⊆ E1') p false (|={E1,∅}=> P) P | |
| (|={E1',E3}=> Q) (|={E1'∖E1,E3}=> Q) | 2. | |
| Proof. |
| scala> import scala.quoted._ | |
| scala> import scala.quoted.staging._ | |
| scala> run[Int]{(given qctx) => { import qctx.tasty.{_, given}; println(('{1}).unseal.showExtractors); '{1}}} | |
| 1 |run[Int]{(given qctx) => { import qctx.tasty.{_, given}; println(('{1}).unseal.showExtractors); '{1}}} | |
| | ^ | |
| |Could not find implicit scala.quoted.staging.Toolbox. | |
| | | |
| |Default toolbox can be instantiated with: |
| Process: coqide [26881] | |
| Path: /Users/USER/*/coqide | |
| Identifier: coqide | |
| Version: 0 | |
| Code Type: X86-64 (Native) | |
| Parent Process: bash [42527] | |
| Responsible: coqide [26881] | |
| User ID: 501 | |
| Date/Time: 2019-11-29 17:12:42.397 +0100 |
| Ltac caseEq f := generalize (refl_equal f); pattern f at -1; case f. | |
| Section str_def. | |
| Variable A : Set. | |
| CoInductive str (A: Set) : Set := | |
| SCons: A -> str A -> str A. |
| Fixpoint fundamental_subtype {Γ T1 i1 T2 i2} (HT: Γ ⊢ₜ T1, i1 <: T2, i2) {struct HT}: | |
| Γ ⊨ T1, i1 <: T2, i2 | |
| with | |
| fundamental_typed {Γ e T} (HT: Γ ⊢ₜ e : T) {struct HT}: | |
| Γ ⊨ e : T. | |
| Proof. | |
| - iInduction HT as [] "IHT". | |
| + by iApply Sub_Refl. | |
| + by iApply Sub_Trans. | |
| + by iIntros "!> **". |
| Require Import ProofIrrelevance. | |
| Section dep_pair. | |
| Context {A : Type} {P : A -> Prop}. | |
| Definition dep_pair := ex_intro P. | |
| Lemma dep_pair_eq (a1 a2 : A) p1 p2: a1 = a2 -> dep_pair a1 p1 = dep_pair a2 p2. | |
| Proof. | |
| intros ->. | |
| (* Now f_equal can reduce the equality to a homogeneous one, so it works. *) |
So, here's a data point. On my 4-core MacBookPro (Intel Core i7 3,1GHz, 16GB RAM), flambda is slower than vanilla on coq-stdpp, which does not use native-compute AFAIK (and comes from many of the same authors as lambda-rust).
To install this coq-stdpp version, you'll have to run first:
opam repo add iris-dev git+https://gitlab.mpi-sws.org/iris/opam.git
With ocaml-base-compiler.4.07.1:
| (* Based on example from | |
| https://coq.github.io/doc/V8.10.0/refman/proof-engine/ssreflect-proof-language.html#contextual-patterns-in-rewrite *) | |
| (* Find `Fail` to see the error *) | |
| From Coq Require Import ssreflect. | |
| Notation "n .+1" := (Datatypes.S n) (at level 2, left associativity, | |
| format "n .+1") : nat_scope. | |
| Axiom addSn : forall m n, m.+1 + n = (m + n).+1. | |
| (* addSn is declared *) | |
| Axiom addn0 : forall m, m + 0 = m. |