Code

Fixed Ingest.v#37

Code

Closed

caldwellb wants to merge 50 commits intofeature/prop-soundnessinQWIRE/VyZX:feature/prop-soundnessfrom maininQWIRE/VyZX:mainCopy head branch name to clipboard

+3,592-6,347

Commits

Commits on Mar 25, 2023

• Fixed Ingest.v

  caldwellb

  committed
  86c6e2b

  Copy full SHA for 86c6e2b

Commits on Apr 5, 2023

• Updated coq-action.yml

  caldwellb

  committed
  17f3197

  Copy full SHA for 17f3197

• Add n_swap_semantics and fill in a_swap_semantics_ind

  Show description for d041c3b
  adrianleh

  committed
  d041c3b

  Copy full SHA for d041c3b

• Finish up hopf rule

  adrianleh

  committed
  a5da012

  Copy full SHA for a5da012

• Improve name checking hook to check more names and ask for reasons to ignore

  adrianleh

  committed
  2dca2a4

  Copy full SHA for 2dca2a4

Commits on Apr 10, 2023

• Add cnot_involutive and cnot_is_cnot_r

  adrianleh

  committed
  fa28797

  Copy full SHA for fa28797

• Clean up gate rules

  adrianleh

  committed
  05a7585

  Copy full SHA for 05a7585

• n_swap progress

  caldwellb

  committed
  0f2c6ae

  Copy full SHA for 0f2c6ae

• b_swap!

  adrianleh

  committed
  bcd3db2

  Copy full SHA for bcd3db2

Commits on Apr 19, 2023

• Add cast_fn_eq_dim het proofs

  adrianleh

  committed
  18ad74e

  Copy full SHA for 18ad74e

• Fix cast_fn_eq_dim usage

  adrianleh

  committed
  c41f24b

  Copy full SHA for c41f24b

• Nice cast tools

  caldwellb

  committed
  d40fc3a

  Copy full SHA for d40fc3a

• Add bottom_to_top_grow_l and top_to_bottom_grow_r

  adrianleh

  committed
  326f5bc

  Copy full SHA for 326f5bc

Commits on Apr 20, 2023

• Fix opaqueness breaking proofs

  adrianleh

  committed
  b1d45d3

  Copy full SHA for b1d45d3

• Add n_cup_helper_grow_l

  adrianleh

  committed
  ae6607d

  Copy full SHA for ae6607d

Commits on Apr 21, 2023

• Refactor cast for proofs to be explicit

  adrianleh

  committed
  40c68d5

  Copy full SHA for 40c68d5

• Auto solve shelved cast goals

  adrianleh

  committed
  65dcbc1

  Copy full SHA for 65dcbc1

• Refactor more parametric cast proof

  adrianleh

  committed
  0c59bf1

  Copy full SHA for 0c59bf1

• Add simpl_casts_in tactic

  adrianleh

  committed
  b3741b9

  Copy full SHA for b3741b9

• rename cast parameters to fit convention

  adrianleh

  committed
  2469ad2

  Copy full SHA for 2469ad2

Commits on Apr 27, 2023

• Add bundle_wires tactic

  adrianleh

  committed
  5ccd82b

  Copy full SHA for 5ccd82b

Commits on Apr 28, 2023

• Progress to n_wrap_under

  adrianleh

  committed
  e0a5aed

  Copy full SHA for e0a5aed

• Add {Z,X}_n_wrap_over_r_base_unswapped

  adrianleh

  committed
  c69a59e

  Copy full SHA for c69a59e

• Add left versions of n_wrap

  adrianleh

  committed
  d3019b2

  Copy full SHA for d3019b2

Commits on May 11, 2023

• Add ZX_semantics notation "⟦ zx ⟧"

  adrianleh

  committed
  7e1ac55

  Copy full SHA for 7e1ac55

Commits on Jun 30, 2023

• Add bell

  adrianleh

  committed
  3243e52

  Copy full SHA for 3243e52

• Simplify bell proof

  adrianleh

  committed
  d3b720a

  Copy full SHA for d3b720a

Commits on Jul 2, 2023

• Remove broken example

  adrianleh

  committed
  0ffa336

  Copy full SHA for 0ffa336

Commits on Jul 7, 2023

• Add completeness.v

  adrianleh

  committed
  aa7e9c4

  Copy full SHA for aa7e9c4

Commits on Jul 10, 2023

• Take .Old out back

  adrianleh

  committed
  bdd5d3c

  Copy full SHA for bdd5d3c

Commits on Oct 4, 2023

• Getting started on the Harny completeness result.

  caldwellb

  committed
  9e0ea5b

  Copy full SHA for 9e0ea5b

Commits on Oct 9, 2023

• Fixed naming, changed harny var defs

  caldwellb

  committed
  4918a35

  Copy full SHA for 4918a35

• Add Harny_k

  adrianleh

  committed
  e30b0ad

  Copy full SHA for e30b0ad

• Improve harny readability

  adrianleh

  committed
  ec1d619

  Copy full SHA for ec1d619

• Add Rsqrt

  adrianleh

  committed
  d7c59fb

  Copy full SHA for d7c59fb

• Added Csqrt

  caldwellb

  committed
  19aab14

  Copy full SHA for 19aab14

• Updated to add Csqrt usage

  caldwellb

  committed
  93320f8

  Copy full SHA for 93320f8

Commits on Oct 10, 2023

• Add harny_simpl

  adrianleh

  committed
  6bbe4b4

  Copy full SHA for 6bbe4b4

• Updated Harny scalars to Complex numbers

  caldwellb

  committed
  7af39c6

  Copy full SHA for 7af39c6

Commits on Oct 11, 2023

• Restoring removed harny_db

  caldwellb

  committed
  81a8d60

  Copy full SHA for 81a8d60

• harny_completeness can use harny_general

  caldwellb

  committed
  5d490cb

  Copy full SHA for 5d490cb

Commits on Oct 13, 2023

• Completeness_BW finished

  caldwellb

  committed
  7747a8e

  Copy full SHA for 7747a8e

Commits on Oct 17, 2023

• Partially completed Nancy completeness result

  caldwellb

  committed
  6a0c19d

  Copy full SHA for 6a0c19d

Commits on Oct 20, 2023

• Nancy completeness result complete

  caldwellb

  committed
  4dca679

  Copy full SHA for 4dca679

Commits on Oct 29, 2023

• Completeness_C done

  caldwellb

  committed
  0e67006

  Copy full SHA for 0e67006

Commits on Nov 13, 2023

• Cleanup completeness, separated computational rules

  caldwellb

  committed
  183ff5b

  Copy full SHA for 183ff5b

• Merge pull request #39 from inQWIRE/completeness

  Show description for 825577b
  caldwellb

  authored
  825577b

  Copy full SHA for 825577b

• Update README.md

  caldwellb

  authored
  ffe315b

  Copy full SHA for ffe315b

• Merge pull request #41 from inQWIRE/caldwellb-patch-1

  Show description for adf56de
  caldwellb

  authored
  adf56de

  Copy full SHA for adf56de

Commits on Jan 15, 2024

• Fix deprecation warnings in SemanticCore.

  adrianleh

  committed
  03e2cdf

  Copy full SHA for 03e2cdf