alxest

(*** Usual, unoptimized tree ***)
type tree =
  | Leaf of int | Node: (tree * tree) -> tree

let gen_tree(): tree =
  let rec _gen_tree (i: int): tree =
    if i > 0
    then Node (_gen_tree(Random.int(i)), _gen_tree(Random.int(i)))
    else Leaf (Random.bits())  in
  (* _gen_tree(Random.int(10000000)) *)

alxest

Require Import Coqlib.
Require Import STS.
Require Import Behavior.
Require Import PCM.
Require Import Any.
Require Import ITreelib.
Require Import AList.
Require Import Coq.Init.Decimal.
Require Export IProp.
Require Import IPM.

alxest

Original Hoareproof0

total time:    131.773s

 tactic                                   local  total   calls       max 
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─steps ---------------------------------   0.1%  80.3%      91   16.762s
─mred ----------------------------------   0.3%  43.1%     619    0.624s
─ired_both -----------------------------   0.1%  40.1%    1815    0.268s
─_prw ----------------------------------   0.4%  40.0%     820    0.246s

alxest

Set Implicit Arguments.
(* #[universes(notemplate)] *) (*** <------- if you uncomment this line, "Let B" below fails ***)
Inductive list2 (X: Type): Type :=
| nil
| cons: X -> list2 X -> list2 X
.
Inductive any: Type := upcast { X: Type; x: X }.
Let A := upcast (nil _: list2 nat).
(*** with template poly    --> no constraint
     without template poly --> (* {} |= list2.u0 <= any.u0 *)

alxest

Require Import sflib.
Require Import ClassicalDescription Lia.

Set Implicit Arguments.



Inductive my_ra: Type :=
| actual (n: nat)
| observed (m: nat)

alxest

Set Printing Universes.



Definition def: Type := Type.
(* {def.u1 def.u0} |= def.u1 < def.u0 *)


Record record: Type := {
  ty: Type;

alxest

Require Import ClassicalDescription.
Require Import Program.
Set Universe Polymorphism.

Inductive Any: Type :=
  Any_intro : forall {A:Type} {x:A}, Any.

Definition downcast (a: Any) (T: Type): option T.
destruct a.
destruct (excluded_middle_informative (A = T)).

alxest

Require Import Program.Tactics.

(***### A new feature in Coq 8.11 ###***)
Unset Universe Checking.
Set Universe Polymorphism.
Set Polymorhpic Inductive Cumulativity.

(***### itree does not support Coq 8.11, so I copy-paste the "ITreeDefinition.v". ###***)

alxest

Require Import Program.
Require Import ZArith.

Class converter (X Y: Type) := { conv: X -> Y }.
Notation "@" := conv (at level 50).

Global Program Instance nat2Z_converter: converter nat Z.
Next Obligation. apply Z.of_nat; auto. Defined.

Global Program Instance Z2nat_converter: converter Z nat.

alxest

[profiler-profile "24.3" memory #s(hash-table size 12466 test equal rehash-size 1.5 rehash-threshold 0.8 data ([message profiler-start call-interactively command-execute execute-extended-command call-interactively nil nil nil nil nil nil nil nil nil nil] 2032 [window-end linum-update-window mapc linum-update linum-update-current nil nil nil nil nil nil nil nil nil nil nil] 687304 ["#<compiled 0x1779f5f>" funcall linum-update-window mapc linum-update linum-after-scroll redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil] 1040 [redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil nil nil] 82933157 [file-readable-p image-search-load-path find-image eval "#<compiled 0x273cbf>" mapcar tool-bar-make-keymap-1 tool-bar-make-keymap redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil] 46306 [file-symlink-p apply tramp-completion-run-real-handler tramp-completion-file-name-handler file-symlink-p file-truename apply tramp-completion-run-real-handler tramp