Code

Program equivalence for Core.Main#2

Code

Draft

lukaszcz wants to merge 32 commits intomainanoma/juvix-lean:mainfrom program-equivalenceanoma/juvix-lean:program-equivalenceCopy head branch name to clipboard

+1,973-170

Commits

Commits on Jan 15, 2025

• Value.Equiv (wip, wrong)

  lukaszcz

  committed
  522f0f2

  Copy full SHA for 522f0f2

• Approx & its monotonicity

  lukaszcz

  committed
  e9caddc

  Copy full SHA for e9caddc

• approx transitivity

  lukaszcz

  committed
  cb10068

  Copy full SHA for cb10068

• refactor (wip, wrong)

  lukaszcz

  committed
  88a3a73

  Copy full SHA for 88a3a73

• Value.Approx correction

  lukaszcz

  committed
  d37aea9

  Copy full SHA for d37aea9

• minor refactor

  lukaszcz

  committed
  a58da50

  Copy full SHA for a58da50

• rename Context to Env

  lukaszcz

  committed
  35846d2

  Copy full SHA for 35846d2

• Eval.Defined

  lukaszcz

  committed
  bfa868b

  Copy full SHA for bfa868b

• Language.Context

  lukaszcz

  committed
  8ef4956

  Copy full SHA for 8ef4956

• approx inversion lemmas

  lukaszcz

  committed
  875e578

  Copy full SHA for 875e578

Commits on Jan 16, 2025

• generalize definitions (wip, not transitive)

  lukaszcz

  committed
  5a440d9

  Copy full SHA for 5a440d9

• CI

  lukaszcz

  committed
  772f247

  Copy full SHA for 772f247

Commits on Jan 23, 2025

• letrec

  lukaszcz

  committed
  c13c8b5

  Copy full SHA for c13c8b5

• indexed evaluation

  lukaszcz

  committed
  de7817a

  Copy full SHA for de7817a

• indexed approximation

  lukaszcz

  committed
  f97d67d

  Copy full SHA for f97d67d

Commits on Jan 24, 2025

• Eval <-> Eval.Indexed

  lukaszcz

  committed
  79c190c

  Copy full SHA for 79c190c

• notation precedences

  lukaszcz

  committed
  bfef1a0

  Copy full SHA for bfef1a0

• notation precedences

  lukaszcz

  committed
  6aee2d7

  Copy full SHA for 6aee2d7

• 'invert' tactic

  lukaszcz

  committed
  8164b76

  Copy full SHA for 8164b76

• anti-monotonicity of indexed approximation

  lukaszcz

  committed
  ca18db5

  Copy full SHA for ca18db5

• args approx

  lukaszcz

  committed
  7367808

  Copy full SHA for 7367808

Commits on Jan 27, 2025

• preservation (wip)

  lukaszcz

  committed
  6af0c2e

  Copy full SHA for 6af0c2e

Commits on Jan 28, 2025

• preservation

  lukaszcz

  committed
  cab1466

  Copy full SHA for cab1466

• contextual equivalence

  lukaszcz

  committed
  dddc659

  Copy full SHA for dddc659

• soundness (wip)

  lukaszcz

  committed
  88ce938

  Copy full SHA for 88ce938

• transitivity

  lukaszcz

  committed
  253307c

  Copy full SHA for 253307c

• closure condition

  lukaszcz

  committed
  d5d2397

  Copy full SHA for d5d2397

Commits on Jan 29, 2025

• unindexed approx preservation

  lukaszcz

  committed
  bc0d59c

  Copy full SHA for bc0d59c

• context definition

  lukaszcz

  committed
  2878847

  Copy full SHA for 2878847

• equivalence transitivity, reflexivity, symmetry

  lukaszcz

  committed
  645fdb9

  Copy full SHA for 645fdb9

• soundness (wip)

  lukaszcz

  committed
  bc0a28e

  Copy full SHA for bc0a28e

• count recursion in the steps

  lukaszcz

  committed
  1f0a5d5

  Copy full SHA for 1f0a5d5